make the maude backend output more deterministic

@traiansf please review

The Maude backend had some issues that were making the output to maude JVM dependent. I added some code whose purpose is to ensure that the ordering and numbering of rules is the same accross different Java versions.
Dwight,

I think you should actually give the rule some name/tag, and them kompile the definition with the --transition option include that name/tag.

Traian, that is needed because the definition of the type checker is in fact non-deterministic :-)  If you have two classes in a cycle, then any of them can be picked first by that rule and reported as being in a cycle.  Making it a transition allows us to see and test  both behaviors.

Grigore


________________________________
From: Traian Florin Șerbănuță [notifications@github.com]
Sent: Tuesday, July 15, 2014 11:55 AM
To: kframework/k
Subject: Re: [k] make the maude backend output more deterministic (#711)


In tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.k:

> @@ -589,7 +589,7 @@ checks for cycles. */
>              ...</classes> _ => .)
>             <out>... .List => ListItem("Class \"" +String Id2String(C)
>                                    +String "\" is in a cycle!\n") </out>
> -       </T>  [structural]
> +       </T>  [transition]


Why transition?

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/711/files#r14947863>.