Merge pull request #105 from ftsrg/xsts-localvars

Local variables and XSTS grammar rework
ftsrg · Feb 22, 2021 · 61b41b0 · 61b41b0
2 parents f747803 + de877a0
commit 61b41b0
Show file tree

Hide file tree

Showing 25 changed files with 1,497 additions and 796 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.10.0"
+    version = "2.11.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsLts.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsLts.java
@@ -13,9 +13,9 @@ public final class XstsLts implements LTS<XstsState, XstsAction> {
 	private final Collection<XstsAction> initActions;
 
 	private XstsLts(final XSTS xsts) {
-		internalActions = xsts.getTransitions().getStmts().stream().map(XstsAction::create).collect(Collectors.toList());
-		externalActions = xsts.getEnvAction().getStmts().stream().map(XstsAction::create).collect(Collectors.toList());
-		initActions = xsts.getInitAction().getStmts().stream().map(XstsAction::create).collect(Collectors.toList());
+		internalActions = xsts.getTran().getStmts().stream().map(XstsAction::create).collect(Collectors.toList());
+		externalActions = xsts.getEnv().getStmts().stream().map(XstsAction::create).collect(Collectors.toList());
+		initActions = xsts.getInit().getStmts().stream().map(XstsAction::create).collect(Collectors.toList());
 	}
 
 	public static LTS<XstsState, XstsAction> create(final XSTS xsts) {

diff --git a/...-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsStateSequence.java b/...-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsStateSequence.java
@@ -9,7 +9,7 @@
 import hu.bme.mit.theta.core.type.inttype.IntLitExpr;
 import hu.bme.mit.theta.xsts.XSTS;
 import hu.bme.mit.theta.xsts.analysis.XstsState;
-import hu.bme.mit.theta.xsts.dsl.TypeDecl;
+import hu.bme.mit.theta.xsts.dsl.XstsTypeDeclSymbol;
 
 import java.util.List;
 import java.util.Optional;
@@ -79,11 +79,13 @@ public String stateToString(ExplState state) {
 			Optional<LitExpr<?>> val = state.eval(decl);
 			if (val.isPresent()) {
 				if (xsts.getVarToType().containsKey(decl)) {
-					TypeDecl type = xsts.getVarToType().get(decl);
+					XstsTypeDeclSymbol type = xsts.getVarToType().get(decl);
 					IntLitExpr intValue = (IntLitExpr) val.get();
-					int index = type.getIntValues().indexOf(intValue.getValue());
-					assert index != -1;
-					sb.add(String.format("(%s %s)", decl.getName(), type.getLiterals().get(index)));
+					var optSymbol = type.getLiterals().stream()
+							.filter(symbol -> symbol.getIntValue().equals(intValue))
+							.findFirst();
+					assert optSymbol.isPresent();
+					sb.add(String.format("(%s %s)", decl.getName(), optSymbol.get().getName()));
 				} else {
 					sb.add(String.format("(%s %s)", decl.getName(), val.get()));
 				}

diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/PnmlTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/PnmlTest.java
@@ -15,27 +15,28 @@
  */
 package hu.bme.mit.theta.xsts.analysis;
 
-import static org.junit.Assert.assertTrue;
-
-import java.io.*;
-import java.util.Arrays;
-import java.util.Collection;
-import hu.bme.mit.theta.analysis.algorithm.*;
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.common.logging.ConsoleLogger;
+import hu.bme.mit.theta.common.logging.Logger;
+import hu.bme.mit.theta.common.logging.Logger.Level;
+import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import hu.bme.mit.theta.xsts.XSTS;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfig;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder;
 import hu.bme.mit.theta.xsts.pnml.PnmlParser;
 import hu.bme.mit.theta.xsts.pnml.PnmlToXSTS;
 import hu.bme.mit.theta.xsts.pnml.elements.PnmlNet;
 import org.junit.Test;
-
-import hu.bme.mit.theta.common.logging.ConsoleLogger;
-import hu.bme.mit.theta.common.logging.Logger;
-import hu.bme.mit.theta.common.logging.Logger.Level;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
 
+import java.io.ByteArrayInputStream;
+import java.io.InputStream;
+import java.util.Arrays;
+import java.util.Collection;
+
+import static org.junit.Assert.assertTrue;
+
 @RunWith(value = Parameterized.class)
 public class PnmlTest {
 
@@ -66,7 +67,7 @@ public static Collection<Object[]> data() {
 	}
 
 	@Test
-	public void test() throws IOException {
+	public void test() {
 
 		try {
 

diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java
@@ -15,28 +15,27 @@
  */
 package hu.bme.mit.theta.xsts.analysis;
 
-import static org.junit.Assert.assertTrue;
-
-import java.io.FileInputStream;
-import java.io.IOException;
-import java.io.InputStream;
-import java.io.SequenceInputStream;
-import java.util.Arrays;
-import java.util.Collection;
-import hu.bme.mit.theta.analysis.algorithm.*;
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.common.logging.ConsoleLogger;
+import hu.bme.mit.theta.common.logging.Logger;
+import hu.bme.mit.theta.common.logging.Logger.Level;
+import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import hu.bme.mit.theta.xsts.XSTS;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfig;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder;
 import hu.bme.mit.theta.xsts.dsl.XstsDslManager;
 import org.junit.Test;
-
-import hu.bme.mit.theta.common.logging.ConsoleLogger;
-import hu.bme.mit.theta.common.logging.Logger;
-import hu.bme.mit.theta.common.logging.Logger.Level;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
 
+import java.io.FileInputStream;
+import java.io.InputStream;
+import java.io.SequenceInputStream;
+import java.util.Arrays;
+import java.util.Collection;
+
+import static org.junit.Assert.assertTrue;
+
 @RunWith(value = Parameterized.class)
 public class XstsTest {
 
@@ -206,13 +205,19 @@ public static Collection<Object[]> data() {
 
 				{ "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.PROD},
 
-				{ "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.PROD_AUTO}
+				{ "src/test/resources/model/array_constant.xsts", "src/test/resources/property/array_constant.prop", true, XstsConfigBuilder.Domain.PROD_AUTO},
+
+				{ "src/test/resources/model/localvars.xsts", "src/test/resources/property/localvars.prop", true, XstsConfigBuilder.Domain.PRED_CART},
+
+				{ "src/test/resources/model/localvars.xsts", "src/test/resources/property/localvars.prop", true, XstsConfigBuilder.Domain.EXPL},
+
+				{ "src/test/resources/model/localvars.xsts", "src/test/resources/property/localvars.prop", true, XstsConfigBuilder.Domain.PROD_AUTO}
 
 		});
 	}
 
 	@Test
-	public void test() throws IOException {
+	public void test() {
 
 		try {
 

diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/localvars.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/localvars.xsts
@@ -0,0 +1,15 @@
+var a: integer = 0
+
+trans {
+    a:=0;
+} or {
+    local var a: integer
+    a:=1;
+}
+
+init {
+    local var a: integer
+    a:=1;
+}
+
+env {}
diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/localvars.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/localvars.prop
@@ -0,0 +1,3 @@
+prop {
+    a==0
+}
diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java
@@ -5,16 +5,15 @@
 import com.beust.jcommander.ParameterException;
 import com.google.common.base.Stopwatch;
 import hu.bme.mit.theta.analysis.Trace;
-import hu.bme.mit.theta.analysis.algorithm.*;
-import hu.bme.mit.theta.analysis.algorithm.cegar.*;
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics;
 import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy;
 import hu.bme.mit.theta.common.CliUtils;
 import hu.bme.mit.theta.common.logging.ConsoleLogger;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.common.logging.NullLogger;
 import hu.bme.mit.theta.common.table.BasicTableWriter;
 import hu.bme.mit.theta.common.table.TableWriter;
-import hu.bme.mit.theta.solver.SolverFactory;
 import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import hu.bme.mit.theta.xsts.XSTS;
 import hu.bme.mit.theta.xsts.analysis.XstsAction;
@@ -23,25 +22,13 @@
 import hu.bme.mit.theta.xsts.analysis.concretizer.XstsTraceConcretizerUtil;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfig;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder;
-import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.Domain;
-import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.Refinement;
-import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.InitPrec;
-import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.PredSplit;
-import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.Search;
+import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.*;
 import hu.bme.mit.theta.xsts.dsl.XstsDslManager;
 import hu.bme.mit.theta.xsts.pnml.PnmlParser;
 import hu.bme.mit.theta.xsts.pnml.PnmlToXSTS;
 import hu.bme.mit.theta.xsts.pnml.elements.PnmlNet;
 
-import java.io.ByteArrayInputStream;
-import java.io.File;
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.IOException;
-import java.io.InputStream;
-import java.io.PrintWriter;
-import java.io.SequenceInputStream;
-import java.io.StringWriter;
+import java.io.*;
 import java.util.concurrent.TimeUnit;
 import java.util.stream.Stream;
 
@@ -252,14 +239,8 @@ private void writeCex(final SafetyResult.Unsafe<?, ?> status, final XSTS xsts) t
 		@SuppressWarnings("unchecked") final Trace<XstsState<?>, XstsAction> trace = (Trace<XstsState<?>, XstsAction>) status.getTrace();
 		final XstsStateSequence concrTrace = XstsTraceConcretizerUtil.concretize(trace, Z3SolverFactory.getInstance(), xsts);
 		final File file = new File(cexfile);
-		PrintWriter printWriter = null;
-		try {
-			printWriter = new PrintWriter(file);
+		try (PrintWriter printWriter = new PrintWriter(file)) {
 			printWriter.write(concrTrace.toString());
-		} finally {
-			if (printWriter != null) {
-				printWriter.close();
-			}
 		}
 	}
 

diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsMetrics.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsMetrics.java
@@ -33,8 +33,8 @@ public static void printMetrics(Logger logger, XSTS xsts){
 		logger.write(Logger.Level.RESULT, "  Bitvector vars: %s%n" , xsts.getVars().stream().filter(v -> v.getType() instanceof BvType).count());
 		logger.write(Logger.Level.RESULT, "  Array vars: %s%n" , xsts.getVars().stream().filter(v -> v.getType() instanceof ArrayType).count());
 		logger.write(Logger.Level.RESULT, "  Ctrl vars: %s%n" , xsts.getCtrlVars().size());
-		logger.write(Logger.Level.RESULT, "Tran statements: %s%n", xsts.getTransitions().accept(StmtCounterVisitor.getInstance(),null));
-		logger.write(Logger.Level.RESULT, "Env statements: %s%n", xsts.getEnvAction().accept(StmtCounterVisitor.getInstance(),null));
-		logger.write(Logger.Level.RESULT, "Init statements: %s%n", xsts.getInitAction().accept(StmtCounterVisitor.getInstance(),null));
+		logger.write(Logger.Level.RESULT, "Tran statements: %s%n", xsts.getTran().accept(StmtCounterVisitor.getInstance(),null));
+		logger.write(Logger.Level.RESULT, "Env statements: %s%n", xsts.getEnv().accept(StmtCounterVisitor.getInstance(),null));
+		logger.write(Logger.Level.RESULT, "Init statements: %s%n", xsts.getInit().accept(StmtCounterVisitor.getInstance(),null));
 	}
 }
diff --git a/subprojects/xsts/xsts/README.md b/subprojects/xsts/xsts/README.md
@@ -56,6 +56,10 @@ When using product abstraction (`PROD`), variables tagged as control variables a
 
 `ctrl var <name> : <type>`
 
+Local variables can be declared at the top of blocks with the `local` keyword. (These variables cannot be flagged as `ctrl` and can have no initial value assigned to them.)
+
+`{ local var <name> : <type> }`
+
 Examples:
 
 ```
@@ -89,6 +93,7 @@ The behaviour of XSTSs can be described using transitions. A transition is an at
 * composite statements:
     * nondeterministic choices of the form `choice { <statement> } or { <statement> }`, with 1 or more branches
     * sequences of the form `<statement> <statement> <statement>`
+    * blocks that can include local variable declarations
 
 Only those branches of a choice statement are considered for execution, of which all contained assumptions evaluate to true.
 
@@ -100,6 +105,8 @@ choice {
     assume y<2;
     x := x+y;
 } or {
+    local var z: integer
+    z := 2;
     choice {
         assume true;
     } or {
-Original file line number
+Diff line change
@@ -0,0 +1,3 @@
+    prop {
+        a==0
+    }