Browse Source

Allow regression test RESULT specifications to refer to pre-defined constants in model/properties file too.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10302 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
commit
ec97c53c0b
  1. 3
      prism/src/prism/PrismCL.java

3
prism/src/prism/PrismCL.java

@ -394,8 +394,7 @@ public class PrismCL implements PrismModelListener
if (test) {
try {
mainLog.println();
Values allConsts = new Values(definedMFConstants);
allConsts.addValues(definedPFConstants);
Values allConsts = new Values(modulesFile.getConstantValues(), propertiesFile.getConstantValues());
if (propertiesToCheck.get(j).checkAgainstExpectedResult(res.getResult(), allConsts)) {
mainLog.println("Testing result: PASS");
} else {

Loading…
Cancel
Save