Model Checkers:
===============

pctl.ptlp:  PCTL model checker
gpl.ptlp:   Model checker for a fragment of GPL

Auxilliary modules for PCTL model checking:
interptrans.P:   Translate reactive-modules-style specification of Markov Chains 
		 to transition relation (rules) used by the PCTL model checker.

------------
*** PCTL ***
------------
Examples for PCTL model checking:
brp.P:      Bounded Retransmission Protocol
leader.P:   Asynchronous Leader Election Protocol
  (both from PRISM Model Checker's Example Suite; 
  see http://www.prismmodelchecker.org/casestudies/)
introex.P:  Example from introduction of Gorlin et al's April 2012 TR

To run these examples:
0. Consult ptlp
1. Load pctl.ptlp (using PTLP's loader, as ptlpload(pctl))
2. For brp and leader, consult interptrans
3. Load example dynamically (e.g load_dyn(brp)).
4. Run top_pmodels(<F>, P), where <F> is a "final" state (e.g. elect for leader)
   as defined the example specification.
5. 


-----------
*** GPL ***
-----------
Examples of GLP model checking:

To run these examples:
0. Consult ptlp
1. Load gpl.ptlp (using PTLP's loader, as ptlpload(gpl))
2. Consult example
3. 


--------------
*** Others ***
--------------
ex5.ptlp:	Direct encoding of reachability checking in an example Markov chain
		(the example chain is same as the one in introex.P)
ex6.ptlp:	Encoding of a Context-Free reachability checker for an example Markov chain.
		