alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

modelcheck: do not load twice model

Browse source 
* tests/ltsmin/modelcheck.cc: Here.
This commit is contained in:
Etienne Renault 2020-06-09 09:01:05 +02:00
parent 4cd23d1fc5
commit d2bde1af19
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
tests/ltsmin/modelcheck.cc
View file

@ -292,7 +292,7 @@ static int checked_main()
} }
} }
if (mc_options.model != nullptr) if (mc_options.model != nullptr && !mc_options.force_parallel)
{ {
tm.start("loading ltsmin model"); tm.start("loading ltsmin model");
try try
@ -327,6 +327,12 @@ static int checked_main()
goto safe_exit; goto safe_exit;
} }
} }
else if (mc_options.force_parallel && mc_options.output)
{
std::cerr << "Cannot combine 'Ouput options' with parallelism.\n"
<< "Consider removing -p.\n";
goto safe_exit;
}
if (mc_options.force_parallel == false && if (mc_options.force_parallel == false &&
mc_options.formula != nullptr && mc_options.formula != nullptr &&