Enter an Orc expression or program (see admissible syntax), or load an example from the right panel.
Add a custom site declaration
Please wait...
Note: The most restrictive limit will be observed if more than one is specified.
(min. 10 seconds, max. 300 seconds)
(Leave blank for no time limit)
Specify an Orc expression pattern (see help) that the solution state must match. Leave blank if no specific pattern is required.
Add a constraint on what values are published
Add a constraint on the number of values published
Add a predicate on the Orc expression of a state
Add a predicate on what values are published
Add a predicate on the number of values published
Specify the LTL formula to verify (see LTL sysntax). Any of the predefined predicates or the custom predicates above may be used.
Total Maude rewrites: rewrite(s) CPU time: second(s)
Powered by jQuery
Developed and maintained by Musab AlTurki