[Help] Understanding the verification engine

[kss682]

Hello,

I'm working with TAPAAL to model a network configuration (schedule) to verify that the message stream satisfy their deadline.
The model is designed as follows:

The system has 2 message streams, both with periodicity of 40 time units and the second stream with a phase of 80 time units.
What I intend to show that when the second stream exist in the network and schedule of the network node is not appropriate then the second stream is bound to miss it's deadline (critical for time sensitive streams). Using this a DeadlineViolated state was formed to check if any packets reach here.

Query: EF TAPN1.DeadlineViolated > 0 then safety is violated.

When using the above query the verification fails for a valid schedule due to random time delay introduced by the verification engine.

I'm trying to understand how the verification engine works. What I would like to verify is that there is no point in the schedule of the messages that they miss the deadline.

Also would be grateful for valuable inputs on these front. I'm also interested in TAPAAL has any sequence diagram support like UPPAAL (that would be something interesting too)

TAPAAL version 4.0.2

Thank you!!