verifyta crashes with a segmentation fault if it is given two arguments: the model and a query file, where the model is a nonexisting file name, but the query file does exist.
I have not been able to reproduce this. I tried with UPPAAL 3.4.10, 3.5.6 and 3.5.7. Running something like verifyta foo fischer.q where foo does not exist but fischer.q does exist produces: behrmann@bugsy:/tmp/uppaal-3.5.6/bin-Linux$ ls fischer.q server socketserver verifyta behrmann@bugsy:/tmp/uppaal-3.5.6/bin-Linux$ ./verifyta bla fischer.q UPPAAL version 3.5.6, Apr 2005 -- verifyta. Compiled with g++-3.4 -O2 -march=pentiumpro -mtune=pentiumpro. Copyright (c) 1995 - 2005, Uppsala University and Aalborg University. All rights reserved. Options for the verification: Diagnostic trace is OFF Search order is breadth first Using conservative space optimisation State space representation uses minimal constraint systems Could not open file to check: No such file or directory
Ah, sorry, I was not clear enough. The extension of the non-existing model seems to be important. Try: verifyta foo.xml fischer.q For me this produces: UPPAAL version 3.5.6, Apr 2005 -- verifyta. Compiled with g++-3.4 -O2 -march=pentiumpro -mtune=pentiumpro. Copyright (c) 1995 - 2005, Uppsala University and Aalborg University. All rights reserved. Options for the verification: Diagnostic trace is OFF Search order is breadth first Using conservative space optimisation State space representation uses minimal constraint systems Verifying property 1 at line 6 zsh: segmentation fault verifyta foo.xml fischer.q Incidentally, it seems verifyta from Uppaal 3.5.7 reports itself as version 3.5.6.
Thanks for the extra information. It is also important that the .q file is "correct without a model", i.e. does not refer to any variables - otherwise verifyta simply complains about syntax errors in .q. Will be fixed for 3.5.8.
A fix has been checked into CVS.