Browse Source

Correct types for initial state of ModulesFile (only a problem when there are clocks).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3298 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
commit
26130c8d38
  1. 18
      prism/src/parser/ast/ModulesFile.java

18
prism/src/parser/ast/ModulesFile.java

@ -790,6 +790,7 @@ public class ModulesFile extends ASTElement
Module module; Module module;
Declaration decl; Declaration decl;
State initialState; State initialState;
Object initialValue;
if (initStates != null) { if (initStates != null) {
return null; return null;
@ -802,7 +803,9 @@ public class ModulesFile extends ASTElement
n = getNumGlobals(); n = getNumGlobals();
for (i = 0; i < n; i++) { for (i = 0; i < n; i++) {
decl = getGlobal(i); decl = getGlobal(i);
initialState.setValue(count++, decl.getStartOrDefault().evaluate(constantValues));
initialValue = decl.getStartOrDefault().evaluate(constantValues);
initialValue = getGlobal(i).getType().castValueTo(initialValue);
initialState.setValue(count++, initialValue);
} }
n = getNumModules(); n = getNumModules();
for (i = 0; i < n; i++) { for (i = 0; i < n; i++) {
@ -810,7 +813,9 @@ public class ModulesFile extends ASTElement
n2 = module.getNumDeclarations(); n2 = module.getNumDeclarations();
for (j = 0; j < n2; j++) { for (j = 0; j < n2; j++) {
decl = module.getDeclaration(j); decl = module.getDeclaration(j);
initialState.setValue(count++, decl.getStartOrDefault().evaluate(constantValues));
initialValue = decl.getStartOrDefault().evaluate(constantValues);
initialValue = module.getDeclaration(j).getType().castValueTo(initialValue);
initialState.setValue(count++, initialValue);
} }
} }
@ -828,6 +833,7 @@ public class ModulesFile extends ASTElement
Module module; Module module;
Declaration decl; Declaration decl;
Values values; Values values;
Object initialValue;
if (initStates != null) { if (initStates != null) {
throw new PrismLangException("There are multiple initial states"); throw new PrismLangException("There are multiple initial states");
@ -840,7 +846,9 @@ public class ModulesFile extends ASTElement
n = getNumGlobals(); n = getNumGlobals();
for (i = 0; i < n; i++) { for (i = 0; i < n; i++) {
decl = getGlobal(i); decl = getGlobal(i);
values.addValue(decl.getName(), decl.getStartOrDefault().evaluate(constantValues));
initialValue = decl.getStartOrDefault().evaluate(constantValues);
initialValue = getGlobal(i).getType().castValueTo(initialValue);
values.addValue(decl.getName(), initialValue);
} }
// then add all module variables // then add all module variables
n = getNumModules(); n = getNumModules();
@ -849,7 +857,9 @@ public class ModulesFile extends ASTElement
n2 = module.getNumDeclarations(); n2 = module.getNumDeclarations();
for (j = 0; j < n2; j++) { for (j = 0; j < n2; j++) {
decl = module.getDeclaration(j); decl = module.getDeclaration(j);
values.addValue(decl.getName(), decl.getStartOrDefault().evaluate(constantValues));
initialValue = decl.getStartOrDefault().evaluate(constantValues);
initialValue = module.getDeclaration(j).getType().castValueTo(initialValue);
values.addValue(decl.getName(), initialValue);
} }
} }

Loading…
Cancel
Save