Maude-help mailing list

["Sung-Shik Jongmans" <S.T.Q.Jongmans AT student.tudelft.nl>]

Title: model-checking versus "normal" rewriting

Hi,

I have a Maude system whose rewrite rules define only one possible behavior (i.e. computation-path) given some initial state q_0. Let <> foo be an LTL property, and let foo be false in the "last" state, say q_n, on the computation-path. Entering:

    Maude> red modelCheck(q_0, <> foo) .

results in a counterexample as expected, and Maude reports that it has performed 18848 rewrites; the counterexample Maude displays is the whole computation path from q_0 up to and including q_n. So far so good :).

However, when I enter:

    Maude> rew q_0 .

Maude reports that is has performed 59203 rewrites, and it displays state q_n. That is, it seems as if Maude required three times more rewrites to get to q_n in this latter case, than that it required to generate the counterexample when model-checking. This appears a bit counterintuitive to me: it would suggest that model-checking in this case is less resource-demanding than "normal" execution, even though the same states are explored.

Could anyone shed some light on what's happening here?

Kind regards,
-Sung.