Maude-help mailing list

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

On 11/10/14 11:27 AM, Diego Marcia wrote:

Hi,
From maude-manual I read that Conditional Rules are subject to "no restriction on which new variables may appear in the righthand side or the condition".
I'm currently trying to pursue a kind of Invariants Model Checking using meta-level operations such as metaSearch and up/downTerm, but when I try to describe the term I'm searching for using new variables I get the error:
variable MyV:MySort is used before it is bound in rule: <MyRule>

I don't get that. Can someone please explain it to me?

Thanks a lot

--

Diego Marcia

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help

If a variable is used before it is bound, you must flag the rule with the nonexec attribute. This means that the rule won't be used for rewriting/searching/model-checking however you can apply from the metalevel the rule using metaApply()/metaXapply(). In this case you are obliged to pass a substitution to bind such variables.

Steven