equal
deleted
inserted
replaced
16 the print_mode facilities provided by Isabelle. <P> |
16 the print_mode facilities provided by Isabelle. <P> |
17 <li>Example: A simple reachability property is formulated in the mu calculus and checked |
17 <li>Example: A simple reachability property is formulated in the mu calculus and checked |
18 by the model checker simply by invoking the tactic mc_tac. |
18 by the model checker simply by invoking the tactic mc_tac. |
19 </UL> |
19 </UL> |
20 |
20 |
21 Note: The example illustrates the use of the print_mode facility even without actually using the model checker. However, if you like to see the example in full functionality, get the Eindhoven model checker from here (<A HREF="http://www4.informatik.tu-muenchen.de/~mueller/tools.html">Eindhoven Model Checker</A>). It is provided as a Sparc SunOS4 binary which also runs under Solaris2.x. |
21 Note: The example illustrates the use of the print_mode facility even without actually using the model checker. However, if you like to see the example in full functionality, get the Eindhoven model checker from here (<A HREF="http://www4.informatik.tu-muenchen.de/~mueller/tools.html">model checker binary</A>) as a Sparc SunOS4 binary which also runs under Solaris2.x, or directly from Eindhoven (<A HREF="http://www.es.ele.tue.nl/geert/research/research_index.html">model checker sources</A>), where you get the C sources and documentation. |
22 |
22 |
23 |
23 |
24 |
24 |
25 </BODY></HTML> |
25 </BODY></HTML> |
26 |
26 |