diff --git a/build.gradle.kts b/build.gradle.kts index f5cf504a48..805daf1ffb 100644 --- a/build.gradle.kts +++ b/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")) } diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/BasicDynamicScope.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/BasicDynamicScope.java new file mode 100644 index 0000000000..4af6fc28da --- /dev/null +++ b/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 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 symbols) { + symbolTable.addAll(symbols); + } + + //// + + @Override + public Optional enclosingScope() { + return enclosingScope; + } + + @Override + public Optional resolve(final String name) { + checkNotNull(name); + final Optional symbol = symbolTable.get(name); + if (symbol.isPresent() || !enclosingScope.isPresent()) { + return symbol; + } else { + return enclosingScope.get().resolve(name); + } + } +} diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/DynamicScope.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/DynamicScope.java new file mode 100644 index 0000000000..348e22009e --- /dev/null +++ b/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 symbols); + + Optional enclosingScope(); + +} diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/SymbolTable.java b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/SymbolTable.java index e06bb73430..9f6d38c3f3 100644 --- a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/dsl/SymbolTable.java +++ b/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); } 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 index daa52a4fbd..1c8de23cfd 100644 --- 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 @@ -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 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()); } + } } 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 index dc90cfd8b1..06b7b4d0bb 100644 --- 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 @@ -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 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 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 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()); + } } } diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/localvars.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/localvars.xsts index 44e2096f5e..b5e5f4c24c 100644 --- a/subprojects/xsts/xsts-analysis/src/test/resources/model/localvars.xsts +++ b/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; } diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/localvars2.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/localvars2.xsts new file mode 100644 index 0000000000..58c836ceab --- /dev/null +++ b/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{} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/localvars2.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/localvars2.prop new file mode 100644 index 0000000000..80f2d856ac --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/localvars2.prop @@ -0,0 +1,3 @@ +prop{ + a==0 +} \ No newline at end of file diff --git a/subprojects/xsts/xsts/README.md b/subprojects/xsts/xsts/README.md index 5c68db18d3..a193970328 100644 --- a/subprojects/xsts/xsts/README.md +++ b/subprojects/xsts/xsts/README.md @@ -56,9 +56,9 @@ When using product abstraction (`PROD`), variables tagged as control variables a `ctrl var : ` -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 : }` +`local var : ` 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 ` := `, where `` is the name of a variable and `` is an expression of the same type * assumptions of the form `assume `, where `` is a boolean expression * havocs of the form `havoc ` + * local variable declarations * composite statements: * nondeterministic choices of the form `choice { } or { }`, with 1 or more branches * sequences of the form ` ` - * 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; diff --git a/subprojects/xsts/xsts/src/main/antlr/XstsDsl.g4 b/subprojects/xsts/xsts/src/main/antlr/XstsDsl.g4 index 7195efd7d4..d7e9e5a89b 100644 --- a/subprojects/xsts/xsts/src/main/antlr/XstsDsl.g4 +++ b/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 diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java index 15b9fe76f0..52ea25a7c3 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java +++ b/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> { - 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); 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 index d88e533566..dff61e390f 100644 --- 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 @@ -1,9 +1,6 @@ package hu.bme.mit.theta.xsts.dsl; -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.VarDecl; import hu.bme.mit.theta.core.dsl.ParseException; import hu.bme.mit.theta.core.stmt.NonDetStmt; @@ -21,7 +18,7 @@ import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; -public class XstsSpecification implements Scope { +public class XstsSpecification implements DynamicScope { private final SymbolTable symbolTable; private final SymbolTable typeTable; @@ -36,7 +33,7 @@ public XstsSpecification(XstsContext context){ } @Override - public Optional enclosingScope() { + public Optional enclosingScope() { return Optional.empty(); } @@ -55,13 +52,13 @@ public XSTS instantiate(){ for(var typeDeclContext: context.typeDeclarations){ final List literals = new ArrayList<>(); for(var literalContext: typeDeclContext.literals){ - var optSymbol = symbolTable.get(literalContext.name.getText()); + var optSymbol = resolve(literalContext.name.getText()); if(optSymbol.isPresent()){ literals.add((XstsTypeLiteralSymbol) optSymbol.get()); } else { var symbol = new XstsTypeLiteralSymbol(literalContext.name.getText()); literals.add(symbol); - symbolTable.add(symbol); + declare(symbol); env.define(symbol,symbol.instantiate()); } } @@ -77,7 +74,7 @@ public XSTS instantiate(){ } final XstsVariableSymbol symbol = new XstsVariableSymbol(typeTable,varDeclContext); - symbolTable.add(symbol); + declare(symbol); final VarDecl var = symbol.instantiate(env); final Optional typeDeclSymbol = typeTable.get(varDeclContext.ttype.getText()); @@ -101,4 +98,14 @@ public XSTS instantiate(){ return new XSTS(varToType,ctrlVars,initSet,tranSet,envSet,initFormula,prop); } + + @Override + public void declare(Symbol symbol) { + symbolTable.add(symbol); + } + + @Override + public void declareAll(Collection symbols) { + symbolTable.addAll(symbols); + } } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java index b4c9349166..63b4090beb 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java @@ -26,11 +26,11 @@ public class XstsStatement { - private final Scope scope; + private final DynamicScope scope; private final SymbolTable typeTable; private final StmtContext context; - public XstsStatement(final Scope scope, final SymbolTable typeTable, final StmtContext context) { + public XstsStatement(final DynamicScope scope, final SymbolTable typeTable, final StmtContext context) { this.scope = checkNotNull(scope); this.typeTable = checkNotNull(typeTable); this.context = checkNotNull(context); @@ -48,25 +48,19 @@ public Stmt instantiate(final Env env) { private static final class StmtCreatorVisitor extends XstsDslBaseVisitor { - private Scope currentScope; + private DynamicScope currentScope; private final SymbolTable typeTable; private final Env env; - public StmtCreatorVisitor(final Scope scope, final SymbolTable typeTable, final Env env) { + public StmtCreatorVisitor(final DynamicScope scope, final SymbolTable typeTable, final Env env) { this.currentScope = checkNotNull(scope); this.typeTable = checkNotNull(typeTable); this.env = checkNotNull(env); } - private void push(final List> localDecls) { - final BasicScope scope = new BasicScope(currentScope); + private void push() { + currentScope = new BasicDynamicScope(currentScope); env.push(); - for (final VarDecl localDecl : localDecls) { - final Symbol symbol = DeclSymbol.of(localDecl); - scope.declare(symbol); - env.define(symbol, localDecl); - } - currentScope = scope; } private void pop() { @@ -133,29 +127,37 @@ public Stmt visitSeqStmt(SeqStmtContext ctx) { } @Override - public Stmt visitBlockStmt(BlockStmtContext ctx) { - if(ctx.varDecls.size()>0){ - final List> localDecls = ctx.varDecls.stream() - .map(d -> createLocalVarDecl(d)).collect(Collectors.toList()); - - push(localDecls); - - final Stmt subStmt = ctx.subStmt.accept(this); + public Stmt visitLocalVarDeclStmt(LocalVarDeclStmtContext ctx) { + final String name = ctx.name.getText(); + final Type type = new XstsType(typeTable,ctx.ttype).instantiate(env); + var decl = Decls.Var(name,type); - pop(); + final Symbol symbol = DeclSymbol.of(decl); + currentScope.declare(symbol); + env.define(symbol, decl); - return subStmt; + if(ctx.initValue==null){ + return SkipStmt.getInstance(); } else { - return ctx.subStmt.accept(this); + var expr = new XstsExpression(currentScope,typeTable,ctx.initValue).instantiate(env); + if (expr.getType().equals(decl.getType())) { + @SuppressWarnings("unchecked") final VarDecl tVar = (VarDecl) decl; + @SuppressWarnings("unchecked") final Expr tExpr = (Expr) expr; + return Assign(tVar, tExpr); + } else { + throw new IllegalArgumentException("Type of " + decl + " is incompatilbe with " + expr); + } } - } - private VarDecl createLocalVarDecl(LocalVarDeclContext ctx){ - final String name = ctx.name.getText(); - final Type type = new XstsType(typeTable,ctx.ttype).instantiate(env); - return Decls.Var(name,type); + @Override + public Stmt visitBlockStmt(BlockStmtContext ctx) { + push(); + final Stmt subStmt = ctx.subStmt.accept(this); + pop(); + return subStmt; } + } } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java index 0276e8c913..ec7fad548b 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java @@ -1,5 +1,6 @@ package hu.bme.mit.theta.xsts.dsl; +import hu.bme.mit.theta.common.dsl.DynamicScope; import hu.bme.mit.theta.common.dsl.Env; import hu.bme.mit.theta.common.dsl.Scope; import hu.bme.mit.theta.common.dsl.SymbolTable; @@ -15,11 +16,11 @@ public class XstsTransitionSet { - private final Scope scope; + private final DynamicScope scope; private final SymbolTable typeTable; private final TransitionSetContext context; - public XstsTransitionSet(final Scope scope, final SymbolTable typeTable, final TransitionSetContext context) { + public XstsTransitionSet(final DynamicScope scope, final SymbolTable typeTable, final TransitionSetContext context) { this.scope = checkNotNull(scope); this.typeTable = checkNotNull(typeTable); this.context = checkNotNull(context);