Is there any way to know if an uppaal model recognizes a trace?

Question

I am trying to check if an uppaal model recognizes a trace.

I have to generate random traces and check if another similar model can do the same trace. I can do the random generation by using verifyta.exe with the query:

" simulate [<=n; 1] {clock} "

However, I do not know if Uppaal or Tron, or some extension is able to check if a model can actually reach the same trace as input. I will appreciate any recommendations, whether it is changing the way I generate the traces or the way I want the models to recognize the traces.

Any help would be highly appreciated :D

Answer 1

First, you need to define what you mean by a trace. The simulate query gives a trajectory of some expressions - this is rarely needed, as it contains very precise information (hardly reproducible in a different system).

Uppaal ECDAR can check the simulation refinement between two processes, and the trace is a timed sequence of actions.

Uppaal TRON is concerned with relativized timed i/o conformance relation, also defined through a timed trace of i/o actions, except the trace is composed interactively where inputs are generated by TRON and outputs by implementation under test. One can also declare that all observable actions are outputs and thus feed the trace from IUT where TRON will check if the trace can be accepted by the model. This is so called monitoring mode and it can be performed by a special "trace adapter" which reads a trace and executes it on the behalf of IUT. TRON distribution contains a few examples driven by a script in trace directory using TraceAdapter. The adapter takes arguments after -- to tron command line and the trace can be fed via standard input stream.