Maude-help mailing list

["Morandi Benjamin" <benjamin.morandi AT inf.ethz.ch>]

Dear All,

 

I am currently experimenting with the built-in LTL model checker to verify properties of concurrent programs, and some questions came up.

 

- 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?

- 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?

- 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?

 

Best regards

 

Benjamin