imitator-model-checker / imitator-web Goto Github PK

The web service expects a property file even when this is not required (for checking syntax, printing the model…)

It would be interesting to have fields for each option of imitator in order to auto-complete the options field in the form. For instance:

• exploration limits: time, states, depth
• output : PTA, PZG, …

It would be interesting to have pre-defined properties, such as:

property := #synth Cycle;

property := #witness Cycle;

property := #synth CycleThrough(accepting);

property := #witness CycleThrough(accepting);

When there is a syntax error in the file, imitator aborts but the web interface requires to click the stop button.

The folder benchmarks of imitator have interesting properties for each model. It would be good to show them as options