Browse Source

Bug fix: PTA model checking using games should complain about not supporting system...endystem.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4526 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
commit
53a05282fa
  1. 5
      prism/src/pta/PTAModelChecker.java

5
prism/src/pta/PTAModelChecker.java

@ -111,6 +111,11 @@ public class PTAModelChecker
// Starting model checking
timer = System.currentTimeMillis();
// Check for system...endsystem - not supported yet
if (modulesFile.getSystemDefn() != null) {
throw new PrismException("The system...endsystem construct is not supported yet (try the digital clocks engine instead)");
}
// Translate ModulesFile object into a PTA object
mainLog.println("\nBuilding PTA...");
m2pta = new Modules2PTA(prism, modulesFile);

Loading…
Cancel
Save