Merge branch 'xstsbugfix'

ftsrg · Sep 13, 2022 · 4cbef24 · 4cbef24
2 parents 577e6c1 + d0409f3
commit 4cbef24
Showing 1 changed file with 5 additions and 4 deletions.
diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java
@@ -87,18 +87,19 @@ public XSTS instantiate(){
 			if(varDeclContext.CTRL()!=null) ctrlVars.add(var);
 			if(varDeclContext.initValue!=null){
 				initExprs.add(Eq(var.getRef(),new XstsExpression(this,typeTable,varDeclContext.initValue).instantiate(env)));
-			} else {
-				initExprs.add(varToType.get(var).createBoundExpr(var));
 			}
 			env.define(symbol,var);
 		}
 
-		final Expr<BoolType> initFormula = ExprUtils.simplify(And(initExprs));
-
 		final NonDetStmt tranSet = new XstsTransitionSet(this,typeTable,context.tran.transitionSet(), varToType).instantiate(env);
 		final NonDetStmt initSet = new XstsTransitionSet(this,typeTable,context.init.transitionSet(), varToType).instantiate(env);
 		final NonDetStmt envSet = new XstsTransitionSet(this,typeTable,context.env.transitionSet(), varToType).instantiate(env);
 
+		for(VarDecl varDecl: varToType.keySet()){
+			initExprs.add(varToType.get(varDecl).createBoundExpr(varDecl));
+		}
+		final Expr<BoolType> initFormula = ExprUtils.simplify(And(initExprs));
+
 		final Expr<BoolType> prop = cast(new XstsExpression(this,typeTable,context.prop).instantiate(env),Bool());
 
 		return new XSTS(varToType,ctrlVars,initSet,tranSet,envSet,initFormula,prop);