Browse Source

Bug fix: experiments not handled correctly in PrismCL when there is a model build failure (e.g. run N=0:4 where 0 causes failure due to empty variable range).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4953 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
commit
6c8ce0b4b5
  1. 13
      prism/src/prism/PrismCL.java

13
prism/src/prism/PrismCL.java

@ -303,7 +303,7 @@ public class PrismCL implements PrismModelListener
// in case of build failure during model checking, store as result for any const values and continue
if (modelBuildFail) {
results[j].setMultipleErrors(definedMFConstants, null, modelBuildException);
continue;
break;
}
// store result of model checking
@ -343,19 +343,14 @@ public class PrismCL implements PrismModelListener
// iterate to next property
undefinedConstants[j].iterateProperty();
}
}
// in case of build failure during model checking, store as result for any further properties, and go on to the next model
// in case of build failure during model checking, store as result for any further properties and continue
if (modelBuildFail) {
for (j++; j < numPropertiesToCheck; j++) {
results[j].setMultipleErrors(definedMFConstants, null, modelBuildException);
}
// iterate to next model
undefinedMFConstants.iterateModel();
for (j = 0; j < numPropertiesToCheck; j++) {
undefinedConstants[j].iterateModel();
}
continue;
}
break;
}
}

Loading…
Cancel
Save