search

UPPAALModelChecker / UPPAAL-Meta

This is the offcial meta repo for issue reporting, feature request and public roadmap for the development of UPPAAL.
http://www.uppaal.org
1 stars 0 forks source link

Emptiness check through terminal #220

Open anirjoshi opened 1 year ago

anirjoshi commented 1 year ago

Is it possible to use terminal commands to do emptiness check for timed automata?

mikucionisaau commented 1 year ago

Could you please elaborate what does emptiness mean in your case?

Uppaal does not implement the notion of acceptance or final states, so it is not clear what you mean. If it means reaching a particular configuration (identified by some state predicate, let's call it acceptance) then one can formulate a query like A[] not acceptance, save it into a file and run verifyta command line utility on your model with that query file and it will output whether the model cannot reach the acceptance state.