Analysis method dependent warnings and errors

[RasmusRendal]

As UPPAAL has grown over the years, it has come to support many more analysis methods. While we initially only had symbolic model checking, this is no longer the case. Furthermore, the Venn Diagram of the models that support symbolic model checking, and the models that support, for instance, SMC, is not a perfect circle.

A user that is explicitly creating a model for SMC should not receive warnings about it not working with classical analysis methods. Therefore, the analysis methods that a TA aims to support should be a part of the document describing it. I propose simply having the <nta> tag at the beginning have optional attributes such as classical="false", which allows the user to disable any warnings and errors related to classical model checking. Otherwise, it should default to true.

Specifically, this would mostly involve killing of the feature checker, since we move that responsibility onto the user. This will increase the usability significantly, because instead of the tab you want to use getting greyed out without knowing why, you will specify what methods you want to use, and if you create a model to which that method isn't applicable, UPPAAL will tell you what you're doing wrong.

Summary for model categories in UTAP (draft):

• is_timed: plain timed automata with simple clocks and integer variables, all kinds of synchronisations, which do not use:

  • Dynamical expressions over simple clock rate (derivative).

  UPPAAL accepts but abstracts away the following features:

  • Dynamical expressions over hybrid clock rates (derivatives) as hybrid clock vairables are removed (abstracted away).
  • Branching edges become non-deterministic edges and probabilistic weights are ignored (abstracted away).
  • Exponential delay rates on locations (abstracted away).
  • Floating point variables (double) and operations (abstracted away).
  • Uncontrollable edges become simple edges (game information is abstracted away).

• is_stopwatch: same as is_timed, but can have clock rate (derivate) expressions which stop the clock, e.g. x'==0 (and x'==1, which is default and can be omitted).

• is_hybrid: same as is_stopwatch, but can have arbitrary clock rate (derivative) expressions. Such models cannot have:

  • Handshake synchronizations (too complicated to determine on-the-fly when synchronizations are available).
  • Guards over dynamical clock variables (non-const derivatives) with non-urgent edges (use ASAP! synchronization to make edge urgent, which is declaraed as urgent broadcast ASAP;).

• is_stochastic: same as is_hybrid, but can have branching edges and exponential delay rates on locations. Such models cannot have:

  • Handshake synchronizations (resulting probability distributions become too complicated to be specified and analysed).
  • Guards over dynamical clock variables (non-const derivatives) with non-urgent edges.

• is_game: same as is_timed but allows more than one player, has non-controllable edges.

[petergjoel]

We probably need to discuss some good and more semantic tags here (e.g. is_timed_automata, is_stopwatch_automata, has_stochastics, ..), but I like the idea.

Also, instead of making this flags in the NTA-tag, maybe add a specific tag such as <semantics> with sub-tags related to which warnings are disabled. Just having attributes seems limiting and probably will need a refactor down the road.

One could e.g. imagine that a is_game can be refined by number_of_players and non_lazy etc.

[RasmusRendal]

Analysis methods shouldn't be the only thing supported this way. For instance, we could also have an option which decided which extrapolation methods should be applicable to the model. However, since 99% the time, the user shouldn't have to know what extrapolation is, we should also have an "automatic" mode, which just silences all errors, and auto-enables the ones that receive none.

I don't think many users would actually care about what extrapolation methods their model supports. But I think moving responsibility for checking which ones are possible to the type checker would be better than what we are doing now.

[mikucionisaau]

I have added a proposal for model categories to the descriptions of this issue.
They are mostly "add-on" for UTAP, whereas UPPAAL will likely need more refined categories (e.g. certain verification options can be supported only when certain features are absent).

Currently is_hybrid and is_stochastic are synonymous, perhaps they need to be merged into one such as is_hybrid_stochastic.

I am a bit skeptical about the inclusion of such information to the XML documents:

• UPPAAL needs to do such analysis every time it compiles a model, regardless of such specification, so it is redundant for UPPAAL.
• The only real use of such information is for the third parties which want some kind of preview without much analysis of their own. If we try to support third parties, then the categories need to be more refined somehow. E.g. there could be flags for C-like code (struct, functions, arrays -- complicated models), integer variables (to differentiate theoretical timed automata without integer variables), clock variables (to denote untimed systems), distinguish broadcast and handshake synchronizations.