MOrc

Are you sure you want to replace the current Orc program with the selected example?

Orc Program

Enter an Orc expression or program (see admissible syntax), or load an example from the right panel.

Custom Sites

Add a custom site declaration

Raw Maude Output

Please wait...

Simulation Limits

Note: The most restrictive limit will be observed if more than one is specified.

Simulation Timeout

(min. 10 seconds, max. 300 seconds)

Search Type

(Leave blank for no time limit)

Search Parameters

(min. 10 seconds, max. 300 seconds)

Orc Expression Pattern

Specify an Orc expression pattern (see help) that the solution state must match. Leave blank if no specific pattern is required.

Publication Constraints

Add a constraint on what values are published

Add a constraint on the number of values published

Model Checking Parameters

(Leave blank for no time limit)

(min. 10 seconds, max. 300 seconds)

Property to Check
Atomic Predicates

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

LTL Formula

Specify the LTL formula to verify (see LTL sysntax). Any of the predefined predicates or the custom predicates above may be used.

Simulation Results

Execution Statistics

Total Maude rewrites: rewrite(s)
CPU time: second(s)

Orc Publications
Resulting Orc expression

Search Results

Search Statistics

Total Maude rewrites: rewrite(s)
CPU time: second(s)

Model Checking Results

Model Checking Statistics

Total Maude rewrites: rewrite(s)
CPU time: second(s)