Spinroot

Mara

Member

Registered: 2012-05-30

Posts: 24

Swarm jobs termination condition

Hi all!
I'm using swarm to perform the verification of a very large model. I was expecting that when a trail file (i.e. a counterexample) was found all the executions should stop.
But this is not happening. This is a little weird, because if I specify 10h of search, and I'm done after 3 hours why keep searching?
Is there some parameters that I can change to change the swarm behaviour? If not, are you planning to modify swarm in this sense? Or I have to manually modify the .pml.swarm file manually to manage this situation (for instance checking for the presence of trail file as a condition to break the execution wait loop)?

Thank you

Mara

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: Swarm jobs termination condition

If I remember correctly, no new jobs shoud be initiated once a trail file exists, but currently running jobs run to completion. We could change that of course. Good candidate for a new update.

Mara

Member

Registered: 2012-05-30

Posts: 24

Re: Swarm jobs termination condition

Yes, you were right, I can control the behaviour of the remaining scripts simply  compiling swarm with the -e flag. But as you pointed out, the already running ones are not affected.
Thank you, as usual
Mara