This file explains how to use the prod CTL model
checker in homework assignment 3.
------------------------------------------------

palmu ~/scratch 85 % use prod
[prod is now in use]
palmu ~/scratch 86 % mkdir mutex_ctl
palmu ~/scratch 87 % cd mutex_ctl
palmu mutex_ctl 88 % cp ~kepa/mutex/mutex.net .
palmu mutex_ctl 89 % prod mutex.init
palmu mutex_ctl 90 % ./mutex -.
.........................
.........................
...................
palmu mutex_ctl 91 % 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(!((pc >= <.0,rem.>) || (pc >= <.1,rem.>) || (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
palmu mutex_ctl 93 %