Merge pull request #107 from ftsrg/xsts-localvars

Improved XSTS local variables

build.gradle.kts

@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.11.1"
+    version = "2.12.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/BasicDynamicScope.java

@@ -0,0 +1,46 @@
+package hu.bme.mit.theta.common.dsl;
+
+import java.util.Collection;
+import java.util.Optional;
+
+import static com.google.common.base.Preconditions.checkNotNull;
+
+public class BasicDynamicScope implements DynamicScope  {
+	private final Optional<DynamicScope> enclosingScope;
+	private final SymbolTable symbolTable;
+
+	public BasicDynamicScope(final DynamicScope enclosingScope) {
+		this.enclosingScope = Optional.ofNullable(enclosingScope);
+		symbolTable = new SymbolTable();
+	}
+
+	////
+
+	@Override
+	public void declare(final Symbol symbol) {
+		symbolTable.add(symbol);
+	}
+
+	@Override
+	public void declareAll(final Collection<? extends Symbol> symbols) {
+		symbolTable.addAll(symbols);
+	}
+
+	////
+
+	@Override
+	public Optional<DynamicScope> enclosingScope() {
+		return enclosingScope;
+	}
+
+	@Override
+	public Optional<? extends Symbol> resolve(final String name) {
+		checkNotNull(name);
+		final Optional<Symbol> symbol = symbolTable.get(name);
+		if (symbol.isPresent() || !enclosingScope.isPresent()) {
+			return symbol;
+		} else {
+			return enclosingScope.get().resolve(name);
+		}
+	}
+}

subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/DynamicScope.java

@@ -0,0 +1,14 @@
+package hu.bme.mit.theta.common.dsl;
+
+import java.util.Collection;
+import java.util.Optional;
+
+public interface DynamicScope extends Scope{
+
+	void declare(final Symbol symbol);
+
+	void declareAll(final Collection<? extends Symbol> symbols);
+
+	Optional<? extends DynamicScope> enclosingScope();
+
+}

subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/SymbolTable.java

@@ -34,7 +34,7 @@ public SymbolTable() {
 
 	public void add(final Symbol symbol) {
 		checkNotNull(symbol);
-		checkArgument(!stringToSymbol.containsKey(symbol.getName()));
+		checkArgument(!stringToSymbol.containsKey(symbol.getName()), String.format("Symbol %s is already declared in this scope",symbol.getName()));
 		stringToSymbol.put(symbol.getName(), symbol);
 	}
 

subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/PnmlTest.java

@@ -29,8 +29,12 @@
 import org.junit.Test;
 import org.junit.runner.RunWith;
 import org.junit.runners.Parameterized;
+import org.xml.sax.SAXException;
 
+import javax.xml.parsers.ParserConfigurationException;
+import javax.xml.xpath.XPathExpressionException;
 import java.io.ByteArrayInputStream;
+import java.io.IOException;
 import java.io.InputStream;
 import java.util.Arrays;
 import java.util.Collection;
@@ -67,34 +71,26 @@ public static Collection<Object[]> data() {
 	}
 
 	@Test
-	public void test() {
+	public void test() throws IOException, XPathExpressionException, SAXException, ParserConfigurationException {
 
-		try {
+		final Logger logger = new ConsoleLogger(Level.SUBSTEP);
 
-			final Logger logger = new ConsoleLogger(Level.SUBSTEP);
+		final PnmlNet pnmlNet = PnmlParser.parse(filePath,initialMarking);
 
-			final PnmlNet pnmlNet = PnmlParser.parse(filePath,initialMarking);
-
-			XSTS xsts = null;
-
-			try (InputStream propStream = new ByteArrayInputStream(("prop { " + targetMarking + " }").getBytes())) {
-				xsts = PnmlToXSTS.createXSTS(pnmlNet, propStream);
-			} catch (Exception e) {
-				e.printStackTrace();
-			}
-
-			final XstsConfig<?, ?, ?> configuration = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()).predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250).initPrec(XstsConfigBuilder.InitPrec.ALLVARS).logger(logger).build(xsts);
-			final SafetyResult<?, ?> status = configuration.check();
-			if (safe) {
-				assertTrue(status.isSafe());
-			} else {
-				assertTrue(status.isUnsafe());
-			}
+		XSTS xsts;
+		try (InputStream propStream = new ByteArrayInputStream(("prop { " + targetMarking + " }").getBytes())) {
+			xsts = PnmlToXSTS.createXSTS(pnmlNet, propStream);
+		}
 
-		} catch (Exception e){
-			e.printStackTrace();
+		final XstsConfig<?, ?, ?> configuration = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()).predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250).initPrec(XstsConfigBuilder.InitPrec.ALLVARS).logger(logger).build(xsts);
+		final SafetyResult<?, ?> status = configuration.check();
+		if (safe) {
+			assertTrue(status.isSafe());
+		} else {
+			assertTrue(status.isUnsafe());
 		}
 
+
 	}
 
 }

subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java

@@ -29,6 +29,7 @@
 import org.junit.runners.Parameterized;
 
 import java.io.FileInputStream;
+import java.io.IOException;
 import java.io.InputStream;
 import java.io.SequenceInputStream;
 import java.util.Arrays;
@@ -149,7 +150,7 @@ public static Collection<Object[]> data() {
 
 				{ "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_5.prop", false, XstsConfigBuilder.Domain.PROD},
 
-				{ "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_50.prop", false, XstsConfigBuilder.Domain.PRED_CART},
+//				{ "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_50.prop", false, XstsConfigBuilder.Domain.PRED_CART},
 
 				{ "src/test/resources/model/counter50.xsts", "src/test/resources/property/x_eq_50.prop", false, XstsConfigBuilder.Domain.EXPL},
 
@@ -175,7 +176,7 @@ public static Collection<Object[]> data() {
 
 				{ "src/test/resources/model/bhmr2007.xsts", "src/test/resources/property/bhmr2007.prop", true, XstsConfigBuilder.Domain.PRED_CART},
 
-				{ "src/test/resources/model/bhmr2007.xsts", "src/test/resources/property/bhmr2007.prop", true, XstsConfigBuilder.Domain.EXPL},
+//				{ "src/test/resources/model/bhmr2007.xsts", "src/test/resources/property/bhmr2007.prop", true, XstsConfigBuilder.Domain.EXPL},
 
 //				{ "src/test/resources/model/bhmr2007.xsts", "src/test/resources/property/bhmr2007.prop", true, XstsConfigBuilder.Domain.PROD},
 
@@ -211,38 +212,35 @@ public static Collection<Object[]> data() {
 
 				{ "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}
+				{ "src/test/resources/model/localvars.xsts", "src/test/resources/property/localvars.prop", true, XstsConfigBuilder.Domain.PROD_AUTO},
 
-		});
-	}
+				{ "src/test/resources/model/localvars2.xsts", "src/test/resources/property/localvars2.prop", true, XstsConfigBuilder.Domain.PRED_CART},
 
-	@Test
-	public void test() {
+				{ "src/test/resources/model/localvars2.xsts", "src/test/resources/property/localvars2.prop", true, XstsConfigBuilder.Domain.EXPL},
 
-		try {
+				{ "src/test/resources/model/localvars2.xsts", "src/test/resources/property/localvars2.prop", true, XstsConfigBuilder.Domain.PROD_AUTO}
 
-			final Logger logger = new ConsoleLogger(Level.SUBSTEP);
 
-			XSTS xsts = null;
+		});
+	}
 
-			try (InputStream inputStream = new SequenceInputStream(new FileInputStream(filePath), new FileInputStream(propPath))) {
-				xsts = XstsDslManager.createXsts(inputStream);
-			} catch (Exception e) {
-				e.printStackTrace();
-			}
+	@Test
+	public void test() throws IOException {
 
-			final XstsConfig<?, ?, ?> configuration = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()).initPrec(XstsConfigBuilder.InitPrec.CTRL).predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250).logger(logger).build(xsts);
-			final SafetyResult<?, ?> status = configuration.check();
-			if (safe) {
-				assertTrue(status.isSafe());
-			} else {
-				assertTrue(status.isUnsafe());
-			}
+		final Logger logger = new ConsoleLogger(Level.SUBSTEP);
 
-		} catch (Exception e){
-			e.printStackTrace();
+		XSTS xsts;
+		try (InputStream inputStream = new SequenceInputStream(new FileInputStream(filePath), new FileInputStream(propPath))) {
+			xsts = XstsDslManager.createXsts(inputStream);
 		}
 
+		final XstsConfig<?, ?, ?> configuration = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()).initPrec(XstsConfigBuilder.InitPrec.CTRL).predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250).logger(logger).build(xsts);
+		final SafetyResult<?, ?> status = configuration.check();
+		if (safe) {
+			assertTrue(status.isSafe());
+		} else {
+			assertTrue(status.isUnsafe());
+		}
 	}
 
 }

subprojects/xsts/xsts-analysis/src/test/resources/model/localvars.xsts

@@ -3,12 +3,12 @@ var a: integer = 0
 trans {
     a:=0;
 } or {
-    local var a: integer
+    local var a: integer;
     a:=1;
 }
 
 init {
-    local var a: integer
+    local var a: integer;
     a:=1;
 }
 

subprojects/xsts/xsts-analysis/src/test/resources/model/localvars2.xsts

@@ -0,0 +1,11 @@
+var a: integer = 0
+
+trans {
+    a:=0;
+    local var a:integer=1;
+    a:=1;
+}
+
+init{}
+
+env{}

subprojects/xsts/xsts-analysis/src/test/resources/property/localvars2.prop

@@ -0,0 +1,3 @@
+prop{
+    a==0
+}

subprojects/xsts/xsts/README.md

@@ -56,9 +56,9 @@ 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 variables can be declared with the `local` keyword. (These variables cannot be flagged as `ctrl`.) As these declarations are statements, they must end with semicolons.
 
-`{ local var <name> : <type> }`
+`local var <name> : <type>`
 
 Examples:
 
@@ -67,6 +67,7 @@ var a : integer
 var b : boolean = false
 var c : Color = RED
 ctrl var x : integer = 0
+local var y : integer = x + 2; 
 ```
 
 All variable names matching the pattern `temp([0-9])+` are reserved for use by the model checker.
@@ -90,10 +91,11 @@ The behaviour of XSTSs can be described using transitions. A transition is an at
     * assignments of the form `<varname> := <expr>`, where `<varname>` is the name of a variable and `<expr>` is an expression of the same type
     * assumptions of the form `assume <expr>`, where `<expr>` is a boolean expression
     * havocs of the form `havoc <varname>`
+    * local variable declarations
 * 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
+    * blocks
 
 Only those branches of a choice statement are considered for execution, of which all contained assumptions evaluate to true.
 
@@ -105,7 +107,7 @@ choice {
     assume y<2;
     x := x+y;
 } or {
-    local var z: integer
+    local var z: integer = x + 4;
     z := 2;
     choice {
         assume true;

subprojects/xsts/xsts/src/main/antlr/XstsDsl.g4

@@ -255,7 +255,8 @@ DEFAULT
 
 // S T A T E M E N T S
 
-stmt:	assignStmt
+stmt:	localVarDeclStmt
+    |   assignStmt
 	|	havocStmt
 	|	assumeStmt
 	|   nonDetStmt
@@ -267,11 +268,11 @@ nonDetStmt
     ;
 
 blockStmt
-    :   LCURLY (varDecls+=localVarDecl)* subStmt=seqStmt RCURLY
+    :   LCURLY subStmt=seqStmt RCURLY
     ;
 
-localVarDecl
-    :   LOCAL VAR name=ID DP ttype=type
+localVarDeclStmt
+    :   LOCAL VAR name=ID DP ttype=type (EQUALS initValue=expr)? SEMICOLON
     ;
 
 seqStmt

subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java

@@ -2,10 +2,7 @@
 
 import com.google.common.collect.ImmutableList;
 import hu.bme.mit.theta.common.Tuple2;
-import hu.bme.mit.theta.common.dsl.Env;
-import hu.bme.mit.theta.common.dsl.Scope;
-import hu.bme.mit.theta.common.dsl.Symbol;
-import hu.bme.mit.theta.common.dsl.SymbolTable;
+import hu.bme.mit.theta.common.dsl.*;
 import hu.bme.mit.theta.core.decl.Decl;
 import hu.bme.mit.theta.core.dsl.ParseException;
 import hu.bme.mit.theta.core.type.Expr;
@@ -44,11 +41,11 @@
 
 final class XstsExpression {
 
-	private final Scope scope;
+	private final DynamicScope scope;
 	private final SymbolTable typeTable;
 	private final ExprContext context;
 
-	public XstsExpression(final Scope scope, final SymbolTable typeTable, final ExprContext context) {
+	public XstsExpression(final DynamicScope scope, final SymbolTable typeTable, final ExprContext context) {
 		this.scope = checkNotNull(scope);
 		this.typeTable = checkNotNull(typeTable);
 		this.context = checkNotNull(context);
@@ -66,11 +63,11 @@ public Expr<?> instantiate(final Env env) {
 
 	private static final class ExprCreatorVisitor extends XstsDslBaseVisitor<Expr<?>> {
 
-		private Scope currentScope;
+		private DynamicScope currentScope;
 		private final SymbolTable typeTable;
 		private final Env env;
 
-		private ExprCreatorVisitor(final Scope scope, final SymbolTable typeTable, final Env env) {
+		private ExprCreatorVisitor(final DynamicScope scope, final SymbolTable typeTable, final Env env) {
 			currentScope = checkNotNull(scope);
 			this.typeTable = checkNotNull(typeTable);
 			this.env = checkNotNull(env);