This file explains how to use the prod CTL model checker in homework assignment 3. ------------------------------------------------ gamma ~/tmp 51 % use prod [prod is now in use] gamma ~/tmp 52 % mkdir mutex_ctl gamma ~/tmp 53 % cd mutex_ctl gamma mutex_ctl 54 % cp ~ini/mutex/mutex.net . gamma mutex_ctl 55 % prod mutex.init gamma mutex_ctl 56 % ./mutex -. ......................... ......................... ................... gamma mutex_ctl 57 % probe mutex 0#statistics Number of nodes: 693 Number of arrows: 2079 Number of terminal nodes: 0 Number of nodes that have been completely processed: 693 Strongly connected components have not been computed 0#look Node 0 next_granted: <.0,0.> pc: <.0,rem.> + <.1,rem.> + <.2,rem.> vars: <.0,3.> + <.1,3.> + <.2,3.> ------------------------------------------------ 0#check ef(next_granted >= <.1,1.>) Check CTL formula. Evaluating atomic subformulas. Evaluating CTL subformulas. Result: true Path: 0 [> 1 [> 4 [> 10 [> 20 [> 38 [> 62 [> 90 [> 120 [> 153 [> 157 [> 197 [> 239 [> 278 [> 282 [> 318 [> 351 [> 387 [> 427 [> 468 [> 507 [> 544 [> 574 [> 604 0#goto 604 604#look Node 604 next_granted: <.1,1.> pc: <.0,leave_exit.> + <.1,leave_exit.> + <.2,leave_exit.> vars: <.0,3.> + <.1,3.> + <.2,3.> ------------------------------------------------ 604#check af(not((pc >= <.0,rem.>) or (pc >= <.1,rem.>) or (pc >= <.2,rem.>))) Check CTL formula. Evaluating atomic subformulas. Evaluating CTL subformulas. Result: true 604#succ Arrow 0: transition rem, precedence class 0 i = 0 to node 635 ------------------------------------------------ Arrow 1: transition rem, precedence class 0 i = 1 to node 636 ------------------------------------------------ Arrow 2: transition rem, precedence class 0 i = 2 to node 637 ------------------------------------------------ Node 604 has 3 successor arrows ------------------------------------------------ 604#quit gamma mutex_ctl 58 %