This file explains how to use the CTL model checker probe of the PROD
system in homework assignment 3 in CC workstations.

The steps to take once you have logged in an Alpha workstation 
(http://www.hut.fi/atk/luokat/maari-a.html): 

- Take prod in use (use prod)
- make a directory for the analysis and copy the Pr/T net model of the
  mutual exclusion algorithm there from ~ini/mutex/mutex.net 
- create the reachability graph of the Pr/T net using prod 
  (prod mutex.init; ./mutex -.)
- Start using the CTL model checker probe
  (probe mutex)
- check the properties (check ctl-formula)
  The CTL syntax used by probe is explained at 
  http://www.tcs.hut.fi/Teaching/T-79.146/ctl-syntax.ps

Below is a sample session. 
------------------------------------------------

malakiitti ~ 51 % use prod
[prod is now in use]
malakiitti ~ 52 % mkdir mutex_ctl
malakiitti ~ 53 % cd mutex_ctl
malakiitti ~/mutex_ctl 54 % cp ~ini/mutex/mutex.net .
malakiitti ~/mutex_ctl 55 %  prod mutex.init
malakiitti ~/mutex_ctl 56 % ./mutex -.
.........................
.........................
...................
malakiitti ~/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
malakiitti ~/mutex_ctl 58 %