This file explains how to use PROD in general. ---------------------------------------------- The PROD software has been installed to the HP and alpha student workstations, such as the "tree" and "element" series of workstations. (If you want to use PROD on your home Linux machine, you can download the PROD source from the following URL: http://www.tcs.hut.fi/prod and follow the installing instructions.) To use PROD on the HP and alpha machines, you need to give the Unix command: use prod It will setup necessary paths and environment variables. A short PROD example run using the dining philosophers net follows: palmu ~ 51 % use prod [prod is now in use] palmu ~ 52 % mkdir prod_nets palmu ~ 53 % cd prod_nets palmu ~/prod_nets 54 % cp $PRODPATH/sample/ph.net . palmu ~/prod_nets 55 % ls -al total 72 drwxr-xr-x 2 kepa users 8192 Oct 24 13:28 . drwxr-xr-x 12 kepa users 8192 Oct 24 13:28 .. -rw-r--r-- 1 kepa users 1220 Oct 24 13:28 ph.net palmu ~/prod_nets 56 % prod ph.init palmu ~/prod_nets 57 % ls -al total 2608 drwxr-xr-x 3 kepa users 8192 Oct 24 13:29 . drwxr-xr-x 12 kepa users 8192 Oct 24 13:28 .. -rwxr-xr-x 1 kepa users 533628 Oct 24 13:29 ph -rw-r--r-- 1 kepa users 235 Oct 24 13:29 ph.dat -rw-r--r-- 1 kepa users 63 Oct 24 13:29 ph.def -rw-r--r-- 1 kepa users 1220 Oct 24 13:28 ph.net drwxr-xr-x 2 kepa users 8192 Oct 24 13:29 ph.src palmu ~/prod_nets 58 % ./ph -m 2000000 -. ........................ palmu ~/prod_nets 59 % probe ph 0#statistics Number of nodes: 242 Number of arrows: 805 Number of terminal nodes: 1 Number of nodes that have been completely processed: 242 Strongly connected components have not been computed 0#look Node 0 thinking: <.1.> + <.2.> + <.3.> + <.4.> + <.5.> forks: <.1.> + <.2.> + <.3.> + <.4.> + <.5.> ------------------------------------------------ 0#succ Arrow 0: transition takeLeft, precedence class 0 ph = 1 to node 1 ------------------------------------------------ Arrow 1: transition takeLeft, precedence class 0 ph = 2 to node 2 ------------------------------------------------ Arrow 2: transition takeLeft, precedence class 0 ph = 3 to node 3 ------------------------------------------------ Arrow 3: transition takeLeft, precedence class 0 ph = 4 to node 4 ------------------------------------------------ Arrow 4: transition takeLeft, precedence class 0 ph = 5 to node 5 ------------------------------------------------ Node 0 has 5 successor arrows ------------------------------------------------ 0#goto 1 1#look Node 1 thinking: <.2.> + <.3.> + <.4.> + <.5.> forks: <.2.> + <.3.> + <.4.> + <.5.> withLeft: <.1.> ------------------------------------------------ 1#sets Strongly connected components have not been computed Special sets: %0: ** terminal nodes ** 1#build volatile %0 91 1 paths ------------------------------------------------ 1#build volatile verbose %0 PATH Node 91 withLeft: <.1.> + <.2.> + <.3.> + <.4.> + <.5.> ------------------------------------------------ 1 paths ------------------------------------------------ 1#quit palmu ~/prod_nets 60 % prod ph.clean palmu ~/prod_nets 61 % ls -al total 104 drwxr-xr-x 3 kepa users 8192 Oct 24 13:30 . drwxr-xr-x 12 kepa users 8192 Oct 24 13:28 .. -rw-r--r-- 1 kepa users 1220 Oct 24 13:28 ph.net drwxr-xr-x 2 kepa users 8192 Oct 24 13:30 ph.src palmu ~/prod_nets 62 % The most often used prod commands: prod netname.init - compiles a net file netname.net into an executable reachability graph generator netname netname -m 2000000 -. - generates the reachability graph using some extra memory for quicker generation (-m 2000000) and printing dots for each 10 processed states (-.) probe netname - investigate the generated reachability graph prod netname.clean - removes all the files generated by "prod netname.init" use this to clean up the diskspace after you have done your analysis The most often used probe commands: statistics - gives out statistics about the generated reachability graph sets - gives out sets containing terminal nodes, and possible counterexample path look - looks at the current node in the reachability graph succ - shows the arrows of the graph leaving current node goto n - goes to node number n in the reachability grap ----------------------------------------------------------------- There is a new CTL model checker in probe. You need to generate the full reachability graph of the system to obtain correct results (i.e. the stubborn set method should not be used). In UNIX, it is used as follows when using the ph.net sample net as an example: prod ph.init ./ph -. probe ph 0#check ef(withLeft >= <.3.>) Check CTL formula. Evaluating atomic subformulas. Evaluating CTL subformulas. Result: true Path: 0 [> 1 [> 6 [> 21 0#look 21 Node 21 thinking: <.4.> + <.5.> forks: <.4.> + <.5.> withLeft: <.1.> + <.2.> + <.3.> ------------------------------------------------ 0#check au(true, withRight >= <.4.>) Check CTL formula. Evaluating atomic subformulas. Evaluating CTL subformulas. Result: false Path: 0 [> 1 [> 6 [> 21 [> 51 [> 91 [> 91 0# The supported formulas are: ax(f), af(f), ag(f), au(f1, f2), ex(f), ef(f), eg(f), and eu(f1, f2). Note the counterexamples and witnesses facility of the model checker for easier debugging of specifications. You might notice that checking the first CTL formula is somewhat slower than subsequent formulas. This is to be expected because the rechability relation is processed into memory before the first formula is checked. --------------------------------------------------------- See files: $PRODPATH/docs/B13.ps $PRODPATH/docs/B13changes.ps for a more thorough explanation of the PROD tool, or email me if you have problems with it. Kepa -- Keijo.Heljanko@hut.fi