Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha68/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha68/ This release has just one change from Alpha67: the incorporation of an LTL model checker for a finite fragment of rewriting logic. To use the model checker you must load the file model-checker.maude You might also want the file dekker.maude that gives a slightly more realistic example of how to use the model checker. The syntax of LTL formula is given in the LTL module. The available operators are: True true False false ~ f not f /\ g and f \/ g or f -> g implies f <-> g iff @ f next (f holds in the next state) [] f always (f holds now and in all future states) <> f eventually (eventually we will reach a state where f holds) f U g strong until (f holds in all states until the first state where g holds and g will eventually hold) f W g weak until (f holds in all states until the first state where g holds but g need not eventually hold) f R g release (g holds now and in all states upto and including the first state in which f holds but f need not eventually hold) The elementary propositions are just terms (often constants) of sort Prop whose semantics are given by the user. Here's an example: mod TEST is inc MODEL-CHECKER . ops s t : -> State . rl s => t . rl t => s . ops a b : -> Prop . eq s |= a = true . eq t |= b = true . endm Here we have a trivial system with just 2 states, s and t, such that s always goes to t and t always goes to s. There are just two propositions, a and b. a is only true in s and b is only true in t. The semantics of propositions are defined by writing equations of the form eq |= = . where evaluates to true when the proposition matching holds in the state matching . It is only necessary to define the true case, anything else is assumed to be false. Note that since propositions can be arbitrary ground terms we can define parameterized families of propositions with a single equation (see the Dekker algorithm example). To check if a given LTL formula holds in the state transition graph from a given starting state we do a reduction: red |= . For example: red s |= [] <> a . *** a holds infinitely often - true red s |= [] <> b . *** b holds infinitely often - true red s |= [] a . *** a always holds - false red s |= [] (a \/ b) . *** (a or b) always holds - true When the formula is false, a counterexample is produced rather than false. A counterexample is an infinite sequence of states that can be generated in the system and which violates the checked property. A counterexample is presented as a pair of finite lists of states. The second list is a infinite cycle; the first list is a sequence that starts from the start state and reaches the first state of the cycle. Counterexamples are returned as terms using the constructors: op nil : -> StateList [ctor] . op __ : StateList StateList -> StateList [ctor assoc id: nil] . op counterExample : StateList StateList -> Result [ctor] . Here's a slightly more complex example: mod TEST2 is inc MODEL-CHECKER . ops a b : -> Prop . ops s t u v : -> State . rl s => t . rl s => u . rl u => v . rl v => s . rl t => s . rl t => t . eq s |= a = true . eq t |= b = true . endm red s |= <>[] b . *** eventually we reach a state where b *** holds forever - false red s |= []<> a . *** a holds infinitely often - false red s |= <>[] b \/ []<> a . *** one or other of the two previous *** formulae holds - true There are a couple of caveats: (1) The set of reachable states must be finite (otherwise the model check may not halt). (2) LTL formula apply to infinite traces; finite traces (i.e. deadlocks) are a problem. This is dealt with by adding self loops to deadlocked states. There is a module LTL-SIMPLIFIER that can optionally be included along with MODEL-CHECKER; it attempts to rearrange and simplify LTL formulae in order to produce smaller Buchi automata. Known problems: =============== (1) The rewrites used to compute transitions in the state graph are not counted. (2) The model checker responds badly to ^C interrupts. (3) Model checking cannot be traced in a useful way. (4) Counterexamples only list states and not labels, rules, or substitutions; already this looks rather ugly so it's not clear just what is the best format for counter-examples. (5) Buchi automaton generation is highly suboptimal (though better than many existing Buchi automaton-based LTL model checkers). This translates to more space/time usage and longer counter-examples than strictly necessary. (6) No self test for Buchi automaton generation; this is the area where unsoundedness is most likely to arise in a Buchi automaton-based LTL model checker. Design Issues ============= There are a number of UI issues with the model checker and Maude in general on which I would like input from Maude users. (1) To what extent should stuff be put in the prelude (e.g. strings) as opposed to in a library file (e.g. this version of the model checker)? (2) Is it the right thing that model checking is done by special reduce semantics for the _|=_ as opposed to special rewrite semantics for this symbol or a special command (like search)? (3) Should counterexamples be returned as terms (can be processed by user code, but ugly) or arbitrary print out (as a side effect but might be more readable)? (4) Would search be better if it were implemented by a special operator that return it's result as a term rather than as a command which prints it's result on the screen? Or should we have a metaSearch operator which works with meta-terms? (5) What info should go into each step of a counterexample? (6) Would it be useful to have a verbose mode where stuff is printed as the model check proceeds? what stuff would be useful? Some possibilities: (a) # states in very weak alternating automaton. (b) # states & # acceptance sets in generalized Buchi automaton. (c) # states and # accepting states in standard Buchi automaton. (d) # states explore in state transition graph. Could also wrap this stuff into the result term. Steven