Verification related problem

[vogelorlll]

Dear UPPAAL team
Hi, I'm a beginner of UPPAAL. I have a question in the verifier part of the software.
I set the option diagnonal trace to fastest. And I check a property, it will generate a fastest trace by verifier. I was wondering whether this trace is the fastest trace of the model. Or I need to verify it further to check its optimality.
Thank you!

[mikucionisaau]

Fastest means taking the least amount of time, so it is optimal in that sense and there is no need for more work.
There can also be multiple fastest traces and Uppaal provides only one of them.

[vogelorlll]

Thank you so much for your reply.

For example, I want to verify the property E<>TA.State, it will generate a trace using 10000 time units if I set diagonal trace to fastest. According to your reply, 10000 is the least time the model will cost to go TA.state. And I don't need to verify the property like E<>TA.State and global_clock < 10000 to ensure the optimality of 10000.

Besides, I didn't get an answer when I verify the second property E<>TA.State and global_clock < 10000. It took too much time and memory. But when I check the first property, it just took about 2 sec and give me a specific trace. Why verifying the second property taking such long time?

Thank you so much!

[mikucionisaau]

When solution does not exist ( TA.State and global_clock < 10000), then UPPAAL needs to examine the whole state space of the model, which can be huge and time consuming.
But when solution exists (TA.State), UPPAAL finds it before it explores entire state space and hence is able to terminate early.

[vogelorlll]

Hi, thank you so much about your reply.

The solution of the second property does not exist. That's to say, if I wait enough time for UPPAAL to examine the whole state space entirely, will it give me the answes 'unsatatisfied' for the second property?

Thank you.

[mikucionisaau]

Yes.

[vogelorlll]

Thanks very much for your reply. It helps a lot.
Best regards.