Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On 8/15/13 2:51 AM, Morandi Benjamin wrote:

- Some model checking runs seem to take days. This could either be due to the size of the semantics (more than 3000 lines of Maude code, about 70 rewrite rules) or because the model checker is stuck somewhere. Is there any way I can find out where the model checker currently is and whether it is making progress?

It's the size of the state space, not the size of the code that counts; if the state space is infinite, model checking won't terminate unless a counter-example is found. If the property you are checking is complex, the LTL -> Buchi Automaton converter may blow up before any rewriting gets done, because this process is worst case double exponential.

  set verbose on .
Will show the number of states in the Buchi Automaton - if it doesn't then its hung in the conversion.

  set show gc on .
Will show the state of memory management at each garbage collect.

- Unlike most of the examples used in the Maude manual, the programs I considered so far do not have infinite runs but terminate when all processes finish their work. Does this cause a problem for the model checker?

No - deadlock states are implicitly converted to loops.

- The semantics I used is not Church-Rosser, i.e., the ordering in which the rewrite rules are chosen can make a difference to the result. Is this a problem for the model checker?

No - it is expected that rules are non-CR; that's why the full state space gets searched.

Steven