Index of /~jad1/comp204/mcheck/

========================================================================

DATA FOR MODEL CHECKER in ML:

getModel.ml
  used to parse and analyze an annotated finite state machine, updated
  to run on SML/NJ 110.0.7

chkModel.ml
  used to determine whether or not input CTL temporal formulae
  holds for a given model

test.ml
  contains CTL formula tested against the model checker

chkModelExt.ml
  translates an extended set of CTL formula to input CTL formulae
  accepted by chkModel.ml

meet.fsm  
  the finite state machine parsed and analyzed by getModel.ml

meet.ctl.exp
  contains and explains the CTL formulae tested against the model
  checker along with its results

meet.gif
  a drawing of the meet.net structure, from the editor xted, used to
  help formulate CTL queries.

README
  text file describing how to run the model checker, also contains sample runs

========================================================================