how to get trace in 2019 new version

[nicy...@gmail.com]

In 2019 new version, i found a new button 'get trace' in verifier, but the question is when i get trace, where the trace file is?? And i didn't find a new tutorial...
And when some properties arent satisfied, simulator doesn't show counter example.

I use Uppaal version 4.1.22 on operating system win10 with Java W.

[Marius Mikučionis]

On Sunday, December 15, 2019 at 7:06:27 AM UTC+1, nicy wrote:
> In 2019 new version, i found a new button 'get trace' in verifier, but the question is when i get trace, where the trace file is??

This button is a shortcut to enable a diagnostic trace (see Options -> Diagnostic trace), which gets loaded into one of simulators.

> And i didn't find a new tutorial...

It's not yet in the tutorial.
The tutorials are in the Documentation section of uppaal.org:

https://www.it.uu.se/research/group/darts/uppaal/documentation.shtml#tutorials

> And when some properties arent satisfied, simulator doesn't show counter example.

Witness trace is generated only in the following situations:

* when there is an error in the model (e.g. variable value overflow), it gets loaded into either symbolic or concrete simulator, depending on the query.

* when E<> is satisfied – an example is loaded into symbolic simulator. If the property does not hold then it makes no sense.

* when A[] is not satisfied – counter example is loaded into symbolic simulator.

* when Pr[...](<>...) or simulate is satisfied – an example is loaded into concrete simulator.

* when Pr[...]([]...) is not satisfied – a counter example is loaded into concrete simulator.

The probabilistic queries are also sensitive to fastest and shortest options: it will yield the best run it has seen.

>
> I use Uppaal version 4.1.22 on operating system win10 with Java W.

There's 4.1.24 which fixes a few issues.

Best regards,
Marius