I tried to run the example models described in section 5.4 of the Reference manual but discovered that the verification of all models failed. Unfortunately I was not able to determine/understand if or why these errors are valid or invalid.
Verifying component external_multiple_out1 results in the queue-full error:
verify: external_multiple_out1: check: deterministic: ok
verify: external_multiple_out1: check: illegal: fail
error: queue full in model external_multiple_out1
/home/pavlov/projects/dezyne/all_events/08_external_multiple_out_events.dzn:25:15: error: queue-full in component "J1"
Verifying component external_multiple_out2 results in the queue-full error:
verify: external_multiple_out2: check: deterministic: ok
verify: external_multiple_out2: check: illegal: fail
error: queue full in model external_multiple_out2
/home/pavlov/projects/dezyne/all_events/08_external_multiple_out_events.dzn:65:15: error: queue-full in component "J2"
Verifying component external_multiple_out3 results in the deadlock error:
verify: external_multiple_out3: check: deterministic: ok
verify: external_multiple_out3: check: illegal: fail
error: queue full in model external_multiple_out3
/home/pavlov/projects/dezyne/all_events/08_external_multiple_out_events.dzn:103:3: error: deadlock
As I am a new member I am only able to add one attachment. Therefore I only attached images a bout the first model.
In case of external ports you need to specify queue size during verification.
For example: path\to\dezyne\ide.cmd verify --queue-size-external=3 -I . path/to/model/forum_model.dzn
You can easily modify VS Code extension command by adding queue size. For more details please type “verify --help”.
Thank you this indeed solved the queue-size error for models external_multiple_out1 and external_multiple_out2 during both verification and simulation.
Unfortunately this results in a new problem in which the simulation of both models cause a deadlock after the first even. De verification on the other hand does not detect a deadlock.
For model external_multiple_out3 the original deadlock has disappeared for the first event but now occurs after the second event during simulation and now the verification also does not detect any deadlock.
I tried different queue sizes but this did not solve the problem.
This is a known bug for the current simulator which has been addressed in the new simulator (which will be available in future release).
It is a rather academic example (two out events on a single modelling event on an external declared port).
When the whole trace is offered to the simulator it works currently, but when single stepping through the trace it reports wrongly a deadlock. (If you ignore the deadlock and just select “r.a” it continues correctly in the ide, just make sure to simulate with extended queue size “simulate --queue-size-external=3”)
