From 3b965630ccfc80584510417109160c2bac694198 Mon Sep 17 00:00:00 2001 From: DoriCz Date: Mon, 18 Dec 2023 20:25:17 +0100 Subject: [PATCH] Control flow splitting for Timed XSTS --- .../expl/ExplStateValuationExtractor.java | 47 ++ .../pred/PredStateValuationExtractor.java | 33 + .../theta/analysis/prod2/Prod2TransFunc.java | 2 +- .../Prod2ExplPredStateValuationExtractor.java | 36 + .../analysis/utils/ValuationExtractor.java | 14 + .../mit/theta/analysis/zone/ZoneInitFunc.java | 26 + .../theta/analysis/zone/ZoneStmtAnalysis.java | 41 ++ .../theta/analysis/zone/ZoneStmtApplier.java | 188 +++++ .../analysis/zone/ZoneStmtInvTransFunc.java | 24 + .../analysis/zone/ZoneStmtTransFunc.java | 24 + .../hu/bme/mit/theta/core/stmt/Stmts.java | 8 + .../theta/core/utils/StmtAtomCollector.java | 4 +- .../core/utils/StmtContainsTimingVisitor.java | 89 +++ .../bme/mit/theta/core/utils/VarPoolUtil.java | 22 +- .../xsts/analysis/XstsInitAbstractor.java | 31 + .../analysis/config/XstsConfigBuilder.java | 2 +- .../combined/XstsCombinedConfigBuilder.java | 474 ++++++++++++ .../XstsCombinedExprTraceChecker.java | 43 ++ .../combined/XstsCombinedPrecRefiner.java | 40 + .../config/combined/XstsLazyLensUtils.java | 185 +++++ .../timed/ControlFlowSplitLazyAbstractor.java | 207 ++++++ .../timed/ControlFlowSplitResult.java | 44 ++ .../analysis/timed/ControlFlowSplitUtil.java | 370 ++++++++++ .../timed/ControlFlowSplitXstsLts.java | 165 +++++ .../timed/TimedXstsActionProjections.java | 166 +++++ .../timed/TimedXstsProd2Analysis.java | 62 ++ .../{clocks => timed}/XstsClockReplacers.java | 7 +- .../TimedXstsCFSplitCombinedAlgTest.java | 127 ++++ .../theta/xsts/analysis/TimedXstsTest.java | 116 +++ .../model/ANTIVAL_CHK_COID_System.xsts | 681 ++++++++++++++++++ .../model/ANTIVAL_CHK_COID_System_timed.xsts | 678 +++++++++++++++++ .../test/resources/model/Crossroad-Theta.xsts | 326 +++++++++ .../model/Crossroad-Theta_timed.xsts | 324 +++++++++ .../src/test/resources/model/clocks.xsts | 38 + .../test/resources/model/xta_to_txsts.xsts | 37 + .../src/test/resources/property/antival1.prop | 3 + .../test/resources/property/antival10.prop | 3 + .../src/test/resources/property/antival2.prop | 3 + .../src/test/resources/property/antival3.prop | 3 + .../src/test/resources/property/antival4.prop | 3 + .../src/test/resources/property/antival5.prop | 3 + .../src/test/resources/property/antival6.prop | 3 + .../src/test/resources/property/antival7.prop | 3 + .../src/test/resources/property/antival8.prop | 3 + .../src/test/resources/property/antival9.prop | 3 + .../resources/property/antival_safety.prop | 13 + .../src/test/resources/property/clocks.prop | 3 + .../resources/property/crossroad_safety.prop | 3 + .../test/resources/property/xta_to_txsts.prop | 3 + .../hu/bme/mit/theta/xsts/cli/XstsCli.java | 31 +- 50 files changed, 4746 insertions(+), 18 deletions(-) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStateValuationExtractor.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStateValuationExtractor.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStateValuationExtractor.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ValuationExtractor.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneInitFunc.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtAnalysis.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtApplier.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtInvTransFunc.java create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtTransFunc.java create mode 100644 subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtContainsTimingVisitor.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsInitAbstractor.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedConfigBuilder.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedExprTraceChecker.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedPrecRefiner.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsLazyLensUtils.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitLazyAbstractor.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitResult.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitUtil.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitXstsLts.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/TimedXstsActionProjections.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/TimedXstsProd2Analysis.java rename subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/{clocks => timed}/XstsClockReplacers.java (92%) create mode 100644 subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsCFSplitCombinedAlgTest.java create mode 100644 subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsTest.java create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/model/ANTIVAL_CHK_COID_System.xsts create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/model/Crossroad-Theta.xsts create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/model/Crossroad-Theta_timed.xsts create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/model/clocks.xsts create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/model/xta_to_txsts.xsts create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival1.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival10.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival2.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival3.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival4.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival5.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival6.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival7.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival8.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival9.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/antival_safety.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/clocks.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/crossroad_safety.prop create mode 100644 subprojects/xsts/xsts-analysis/src/test/resources/property/xta_to_txsts.prop diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStateValuationExtractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStateValuationExtractor.java new file mode 100644 index 0000000000..a380ef5bb5 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStateValuationExtractor.java @@ -0,0 +1,47 @@ +package hu.bme.mit.theta.analysis.expl; + +import hu.bme.mit.theta.analysis.utils.ValuationExtractor; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.ImmutableValuation; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.LitExpr; + +import java.util.Collection; +import java.util.Map; + +public final class ExplStateValuationExtractor implements ValuationExtractor { + + private static final class LazyHolder { + private static final ExplStateValuationExtractor INSTANCE = new ExplStateValuationExtractor(); + } + + private ExplStateValuationExtractor() { + } + + public static ExplStateValuationExtractor getInstance() { + return ExplStateValuationExtractor.LazyHolder.INSTANCE; + } + + @Override + public Valuation extractValuation(ExplState state) { + return state.getVal(); + } + + @Override + public Valuation extractValuationForVars(ExplState state, Collection> vars) { + + final ImmutableValuation.Builder builder = ImmutableValuation.builder(); + + final Map, LitExpr> varToValue = state.getVal().toMap(); + + for (final VarDecl varDecl : vars) { + final LitExpr value = varToValue.get(varDecl); + if (value != null) { + builder.put(varDecl, value); + } + } + + return builder.build(); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStateValuationExtractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStateValuationExtractor.java new file mode 100644 index 0000000000..7de8d55be0 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStateValuationExtractor.java @@ -0,0 +1,33 @@ +package hu.bme.mit.theta.analysis.pred; + +import hu.bme.mit.theta.analysis.utils.ValuationExtractor; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.ImmutableValuation; +import hu.bme.mit.theta.core.model.Valuation; + +import java.util.Collection; + +public final class PredStateValuationExtractor implements ValuationExtractor { + + private static final class LazyHolder { + private static final PredStateValuationExtractor INSTANCE = new PredStateValuationExtractor(); + } + + private PredStateValuationExtractor() { + } + + public static PredStateValuationExtractor getInstance() { + return PredStateValuationExtractor.LazyHolder.INSTANCE; + } + + + @Override + public Valuation extractValuation(PredState state) { + return ImmutableValuation.empty(); + } + + @Override + public Valuation extractValuationForVars(PredState state, Collection> vars) { + return ImmutableValuation.empty(); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/Prod2TransFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/Prod2TransFunc.java index 80a21176ae..faee5c6496 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/Prod2TransFunc.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/Prod2TransFunc.java @@ -26,7 +26,7 @@ import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.TransFunc; -final class Prod2TransFunc +public final class Prod2TransFunc implements TransFunc, A, Prod2Prec> { private final TransFunc transFunc1; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStateValuationExtractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStateValuationExtractor.java new file mode 100644 index 0000000000..5d73ee6378 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/prod2explpred/Prod2ExplPredStateValuationExtractor.java @@ -0,0 +1,36 @@ +package hu.bme.mit.theta.analysis.prod2.prod2explpred; + +import hu.bme.mit.theta.analysis.expl.ExplState; +import hu.bme.mit.theta.analysis.expl.ExplStateValuationExtractor; +import hu.bme.mit.theta.analysis.pred.PredState; +import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.analysis.utils.ValuationExtractor; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.Valuation; + +import java.util.Collection; + +public class Prod2ExplPredStateValuationExtractor implements ValuationExtractor> { + + private final ExplStateValuationExtractor explValExtractor; + + private Prod2ExplPredStateValuationExtractor(final ExplStateValuationExtractor explValExtractor) { + this.explValExtractor = explValExtractor; + } + + public static Prod2ExplPredStateValuationExtractor create(final ExplStateValuationExtractor explStateValExtractor) { + return new Prod2ExplPredStateValuationExtractor(explStateValExtractor); + } + + @Override + public Valuation extractValuation(Prod2State state) { + final ExplState explState = state.getState1(); + return explValExtractor.extractValuation(explState); + } + + @Override + public Valuation extractValuationForVars(Prod2State state, Collection> vars) { + final ExplState explState = state.getState1(); + return explValExtractor.extractValuationForVars(explState, vars); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ValuationExtractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ValuationExtractor.java new file mode 100644 index 0000000000..95826b1caf --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ValuationExtractor.java @@ -0,0 +1,14 @@ +package hu.bme.mit.theta.analysis.utils; + +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.Valuation; + +import java.util.Collection; + +public interface ValuationExtractor { + + Valuation extractValuation(final S state); + + Valuation extractValuationForVars(final S state, final Collection> vars); +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneInitFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneInitFunc.java new file mode 100644 index 0000000000..ce03cac6c2 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneInitFunc.java @@ -0,0 +1,26 @@ +package hu.bme.mit.theta.analysis.zone; + +import hu.bme.mit.theta.analysis.InitFunc; + +import java.util.Collection; +import java.util.Collections; + +import static com.google.common.base.Preconditions.checkNotNull; + +public class ZoneInitFunc implements InitFunc { + + private static final ZoneInitFunc INSTANCE = new ZoneInitFunc(); + + private ZoneInitFunc() { + } + + public static ZoneInitFunc getInstance() { + return INSTANCE; + } + + @Override + public Collection getInitStates(ZonePrec prec) { + checkNotNull(prec); + return Collections.singleton(ZoneState.zero(prec.getVars()).transform().up().build()); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtAnalysis.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtAnalysis.java new file mode 100644 index 0000000000..0cce7b98bf --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtAnalysis.java @@ -0,0 +1,41 @@ +package hu.bme.mit.theta.analysis.zone; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.InitFunc; +import hu.bme.mit.theta.analysis.PartialOrd; +import hu.bme.mit.theta.analysis.TransFunc; +import hu.bme.mit.theta.analysis.expr.StmtAction; + +public class ZoneStmtAnalysis implements Analysis { + + private static final ZoneStmtAnalysis INSTANCE = new ZoneStmtAnalysis(); + + private final PartialOrd partialOrd; + private final InitFunc initFunc; + private final TransFunc transFunc; + + private ZoneStmtAnalysis() { + this.partialOrd = ZoneOrd.getInstance(); + this.initFunc = ZoneInitFunc.getInstance(); + this.transFunc = ZoneStmtTransFunc.getInstance(); + } + + public static ZoneStmtAnalysis getInstance() { + return INSTANCE; + } + + @Override + public PartialOrd getPartialOrd() { + return partialOrd; + } + + @Override + public InitFunc getInitFunc() { + return initFunc; + } + + @Override + public TransFunc getTransFunc() { + return transFunc; + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtApplier.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtApplier.java new file mode 100644 index 0000000000..a8ae702980 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtApplier.java @@ -0,0 +1,188 @@ +package hu.bme.mit.theta.analysis.zone; + +import com.google.common.collect.Lists; +import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.core.clock.constr.ClockConstrs; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.stmt.*; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.clocktype.ClockConstraintExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockType; +import hu.bme.mit.theta.core.utils.ExprUtils; + +import java.util.List; + +public class ZoneStmtApplier { + + private static final ZonePostStmtVisitor POST_VISITOR = new ZonePostStmtVisitor(); + private static final ZonePreStmtVisitor PRE_VISITOR = new ZonePreStmtVisitor(); + + private ZoneStmtApplier() { + } + + public static ZoneState post(final ZoneState state, final StmtAction action, ZonePrec prec) { + final ZoneState.Builder builder = state.project(prec.getVars()); + final List stmts = action.getStmts(); + for (final Stmt stmt : stmts) { + stmt.accept(POST_VISITOR, builder); + } + return builder.build(); + } + + public static ZoneState pre(final ZoneState state, final StmtAction action, ZonePrec prec) { + final ZoneState.Builder builder = state.project(prec.getVars()); + final List stmts = Lists.reverse(action.getStmts()); + for (final Stmt stmt : stmts) { + stmt.accept(PRE_VISITOR, builder); + } + return builder.build(); + } + + /// + + private static class ZonePostStmtVisitor implements StmtVisitor { + + private ZonePostStmtVisitor() { + } + + @Override + public Void visit(SkipStmt stmt, ZoneState.Builder builder) { + return null; + } + + @Override + public Void visit(AssumeStmt stmt, ZoneState.Builder builder) { + applyAssume(stmt, builder); + return null; + } + + @Override + public Void visit(AssignStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(HavocStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(SequenceStmt stmt, ZoneState.Builder builder) { + stmt.getStmts().forEach(subStmt -> subStmt.accept(this, builder)); + return null; + } + + @Override + public Void visit(NonDetStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(OrtStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(LoopStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(IfStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(DelayStmt stmt, ZoneState.Builder builder) { + builder.nonnegative(); + builder.up(); + return null; + } + + @Override + public Void visit(ResetStmt stmt, ZoneState.Builder builder) { + builder.reset(stmt.getClockDecl(), stmt.getValue()); + return null; + } + } + + /// + + private static class ZonePreStmtVisitor implements StmtVisitor { + + private ZonePreStmtVisitor() { + } + + @Override + public Void visit(SkipStmt stmt, ZoneState.Builder builder) { + return null; + } + + @Override + public Void visit(AssumeStmt stmt, ZoneState.Builder builder) { + applyAssume(stmt, builder); + return null; + } + + @Override + public Void visit(AssignStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(HavocStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(SequenceStmt stmt, ZoneState.Builder builder) { + Lists.reverse(stmt.getStmts()).forEach(subStmt -> subStmt.accept(this, builder)); + return null; + } + + @Override + public Void visit(NonDetStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(OrtStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(LoopStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(IfStmt stmt, ZoneState.Builder builder) { + throw new UnsupportedOperationException(); + } + + @Override + public Void visit(DelayStmt stmt, ZoneState.Builder builder) { + builder.down(); + builder.nonnegative(); + return null; + } + + @Override + public Void visit(ResetStmt stmt, ZoneState.Builder builder) { + final VarDecl clock = stmt.getClockDecl(); + final int value = stmt.getValue(); + builder.and(ClockConstrs.Eq(clock, value)); + builder.free(clock); + return null; + } + } + + /// + + private static void applyAssume(AssumeStmt stmt, ZoneState.Builder builder) { + ExprUtils.getConjuncts(stmt.getCond()).stream() + .filter(cond -> cond instanceof ClockConstraintExpr) + .map(cond -> ClockConstrs.fromClockExpr((ClockConstraintExpr) cond)) + .forEach(builder::and); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtInvTransFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtInvTransFunc.java new file mode 100644 index 0000000000..7f0e9d307d --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtInvTransFunc.java @@ -0,0 +1,24 @@ +package hu.bme.mit.theta.analysis.zone; + +import hu.bme.mit.theta.analysis.InvTransFunc; +import hu.bme.mit.theta.analysis.expr.StmtAction; + +import java.util.Collection; +import java.util.Collections; + +public class ZoneStmtInvTransFunc implements InvTransFunc { + + private final static ZoneStmtInvTransFunc INSTANCE = new ZoneStmtInvTransFunc(); + + private ZoneStmtInvTransFunc() { + } + + public static ZoneStmtInvTransFunc getInstance() { + return INSTANCE; + } + + @Override + public Collection getPreStates(ZoneState state, StmtAction action, ZonePrec prec) { + return Collections.singleton(ZoneStmtApplier.pre(state, action, prec)); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtTransFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtTransFunc.java new file mode 100644 index 0000000000..ce1215b1e8 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneStmtTransFunc.java @@ -0,0 +1,24 @@ +package hu.bme.mit.theta.analysis.zone; + +import hu.bme.mit.theta.analysis.TransFunc; +import hu.bme.mit.theta.analysis.expr.StmtAction; + +import java.util.Collection; +import java.util.Collections; + +public class ZoneStmtTransFunc implements TransFunc { + + private final static ZoneStmtTransFunc INSTANCE = new ZoneStmtTransFunc(); + + private ZoneStmtTransFunc() { + } + + public static ZoneStmtTransFunc getInstance() { + return INSTANCE; + } + + @Override + public Collection getSuccStates(ZoneState state, StmtAction action, ZonePrec prec) { + return Collections.singleton(ZoneStmtApplier.post(state, action, prec)); + } +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java index cc4f0a8918..419507ce9a 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java @@ -56,4 +56,12 @@ public static NonDetStmt NonDetStmt(final List stmts) { return NonDetStmt.of(stmts); } + public static IfStmt IfStmt(final Expr cond, final Stmt then) { + return IfStmt.of(cond, then); + } + + public static IfStmt IfStmt(final Expr cond, final Stmt then, final Stmt elze) { + return IfStmt.of(cond, then, elze); + } + } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAtomCollector.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAtomCollector.java index 0b6e79d7ea..44cd52010c 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAtomCollector.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAtomCollector.java @@ -102,12 +102,12 @@ public Void visit(IfStmt stmt, Set> atoms) { @Override public Void visit(DelayStmt stmt, Set> atoms) { - throw new UnsupportedOperationException(); + return null; } @Override public Void visit(ResetStmt stmt, Set> atoms) { - throw new UnsupportedOperationException(); + return null; } } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtContainsTimingVisitor.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtContainsTimingVisitor.java new file mode 100644 index 0000000000..e84690dd8c --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtContainsTimingVisitor.java @@ -0,0 +1,89 @@ +package hu.bme.mit.theta.core.utils; + +import hu.bme.mit.theta.core.stmt.*; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.clocktype.ClockType; + +import java.util.Collection; + +import static hu.bme.mit.theta.core.stmt.Stmts.Assume; + +// handles delay stmts correctly +public class StmtContainsTimingVisitor implements StmtVisitor { + + private static final class LazyHolder { + private final static StmtContainsTimingVisitor INSTANCE = new StmtContainsTimingVisitor(); + } + + private StmtContainsTimingVisitor() { + } + + public static StmtContainsTimingVisitor getInstance() { + return StmtContainsTimingVisitor.LazyHolder.INSTANCE; + } + + @Override + public Boolean visit(SkipStmt stmt, Void param) { + return false; + } + + @Override + public Boolean visit(AssumeStmt stmt, Void param) { + return containsClockVar(stmt); + } + + @Override + public Boolean visit(AssignStmt stmt, Void param) { + return containsClockVar(stmt); + } + + @Override + public Boolean visit(HavocStmt stmt, Void param) { + return containsClockVar(stmt); + } + + @Override + public Boolean visit(SequenceStmt stmt, Void param) { + return anyStmtContainsTiming(stmt.getStmts()); + } + + @Override + public Boolean visit(NonDetStmt stmt, Void param) { + return anyStmtContainsTiming(stmt.getStmts()); + } + + @Override + public Boolean visit(OrtStmt stmt, Void param) { + return anyStmtContainsTiming(stmt.getStmts()); + } + + @Override + public Boolean visit(LoopStmt stmt, Void param) { + return stmt.getStmt().accept(this, null); + } + + @Override + public Boolean visit(IfStmt stmt, Void param) { + return Assume(stmt.getCond()).accept(this, null) + || stmt.getThen().accept(this, null) + || stmt.getElze().accept(this, null); + } + + @Override + public Boolean visit(DelayStmt stmt, Void param) { + return true; + } + + @Override + public Boolean visit(ResetStmt stmt, Void param) { + return true; + } + + private boolean containsClockVar(final Stmt stmt) { + return StmtUtils.getVars(stmt).stream().anyMatch(v -> v.getType() instanceof ClockType); + } + + private boolean anyStmtContainsTiming(final Collection stmts) { + return stmts.stream().anyMatch(stmt -> stmt.accept(this, null)); + } +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarPoolUtil.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarPoolUtil.java index 6c2bcdd8c6..71f2fae708 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarPoolUtil.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarPoolUtil.java @@ -2,25 +2,37 @@ import hu.bme.mit.theta.core.decl.Decls; import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.inttype.IntType; import java.util.ArrayDeque; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; public class VarPoolUtil { private VarPoolUtil() {} - private static ArrayDeque> intPool=new ArrayDeque>(); - private static int counter=0; + private static ArrayDeque> boolPool = new ArrayDeque>(); + private static ArrayDeque> intPool = new ArrayDeque>(); + private static int counter = 0; - public static VarDecl requestInt(){ - if(intPool.isEmpty()) return Decls.Var("temp"+counter++,Int()); + public static VarDecl requestBool() { + if(boolPool.isEmpty()) return Decls.Var("temp"+counter++, Bool()); + else return boolPool.remove(); + } + + public static VarDecl requestInt() { + if(intPool.isEmpty()) return Decls.Var("temp"+counter++, Int()); else return intPool.remove(); } - public static void returnInt(VarDecl var){ + public static void returnBool(VarDecl var) { + if(!boolPool.contains(var)) boolPool.addFirst(var); + } + + public static void returnInt(VarDecl var) { if(!intPool.contains(var)) intPool.addFirst(var); } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsInitAbstractor.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsInitAbstractor.java new file mode 100644 index 0000000000..be701bd053 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsInitAbstractor.java @@ -0,0 +1,31 @@ +package hu.bme.mit.theta.xsts.analysis; + +import hu.bme.mit.theta.analysis.algorithm.lazy.InitAbstractor; +import hu.bme.mit.theta.analysis.expr.ExprState; + +import static com.google.common.base.Preconditions.checkNotNull; + +public final class XstsInitAbstractor + implements InitAbstractor, XstsState> { + + private final InitAbstractor initAbstractor; + + private XstsInitAbstractor(final InitAbstractor initAbstractor) { + this.initAbstractor = checkNotNull(initAbstractor); + } + + public static XstsInitAbstractor + create(final InitAbstractor initAbstractor) { + return new XstsInitAbstractor<>(initAbstractor); + } + + @Override + public XstsState getInitAbstrState(XstsState concrXstsState) { + final SConcr concrState = concrXstsState.getState(); + final SAbstr abstrState = initAbstractor.getInitAbstrState(concrState); + final boolean lastActionWasEnv = concrXstsState.lastActionWasEnv(); + final boolean isInitialized = concrXstsState.isInitialized(); + final XstsState abstrXstsState = XstsState.of(abstrState, lastActionWasEnv, isInitialized); + return abstrXstsState; + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java index 0d3fb2f5bb..f225115ff6 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java @@ -80,7 +80,7 @@ import hu.bme.mit.theta.xsts.analysis.autoexpl.XstsNewAtomsAutoExpl; import hu.bme.mit.theta.xsts.analysis.autoexpl.XstsNewOperandsAutoExpl; import hu.bme.mit.theta.xsts.analysis.autoexpl.XstsStaticAutoExpl; -import hu.bme.mit.theta.xsts.analysis.clocks.XstsClockReplacers; +import hu.bme.mit.theta.xsts.analysis.timed.XstsClockReplacers; import hu.bme.mit.theta.xsts.analysis.initprec.XstsAllVarsInitPrec; import hu.bme.mit.theta.xsts.analysis.initprec.XstsCtrlInitPrec; import hu.bme.mit.theta.xsts.analysis.initprec.XstsEmptyInitPrec; diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedConfigBuilder.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedConfigBuilder.java new file mode 100644 index 0000000000..ab8fe33ccb --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedConfigBuilder.java @@ -0,0 +1,474 @@ +package hu.bme.mit.theta.xsts.analysis.config.combined; + +import hu.bme.mit.theta.analysis.*; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; +import hu.bme.mit.theta.analysis.algorithm.SearchStrategy; +import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor; +import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; +import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +import hu.bme.mit.theta.analysis.algorithm.lazy.*; +import hu.bme.mit.theta.analysis.algorithm.lazy.itp.*; +import hu.bme.mit.theta.analysis.expl.*; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; +import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.analysis.expr.refinement.*; +import hu.bme.mit.theta.analysis.pred.*; +import hu.bme.mit.theta.analysis.prod2.*; +import hu.bme.mit.theta.analysis.prod2.prod2explpred.*; +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; +import hu.bme.mit.theta.analysis.utils.ValuationExtractor; +import hu.bme.mit.theta.analysis.zone.*; +import hu.bme.mit.theta.common.Tuple4; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.common.logging.NullLogger; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; +import hu.bme.mit.theta.core.utils.Lens; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverFactory; +import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.*; +import hu.bme.mit.theta.xsts.analysis.timed.*; +import hu.bme.mit.theta.xsts.analysis.config.XstsConfig; +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder; + +import java.util.Collection; +import java.util.Set; +import java.util.function.Function; +import java.util.function.Predicate; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Clock; +import static hu.bme.mit.theta.core.utils.TypeUtils.cast; + +@SuppressWarnings({"rawtypes", "unchecked"}) +public final class XstsCombinedConfigBuilder { + + public enum Search { + BFS(SearchStrategy.BFS), + + DFS(SearchStrategy.DFS); + + public final SearchStrategy strategy; + + private Search(final SearchStrategy strategy) { + this.strategy = strategy; + } + } + + public enum ZoneRefinement { + BW_ITP, FW_ITP + } + + public enum ClockStrategy { + + NONE(XstsClockReplacers.None(), false, false), + + INT(XstsClockReplacers.Int(), false, false), + + RAT(XstsClockReplacers.Rat(), false, false), + + CF_SPLIT_ALL(XstsClockReplacers.None(), true, false), + + CF_SPLIT_FILTERCF(XstsClockReplacers.None(), true, true); + + public final XstsClockReplacers.XstsClockReplacer clockReplacer; + public final boolean controlFlowSplitting; + public final boolean filterInfeasibleCF; + + private ClockStrategy(final XstsClockReplacers.XstsClockReplacer clockReplacer, final boolean controlFlowSplitting, final boolean filterInfeasibleCF) { + this.clockReplacer = clockReplacer; + this.controlFlowSplitting = controlFlowSplitting; + this.filterInfeasibleCF = filterInfeasibleCF; + } + } + + private Logger logger = NullLogger.getInstance(); + private final SolverFactory solverFactory; + private final XstsConfigBuilder.Domain domain; + private final XstsConfigBuilder.Refinement refinement; + private Search search = Search.BFS; + private XstsConfigBuilder.PredSplit predSplit = XstsConfigBuilder.PredSplit.WHOLE; + private int maxEnum = 0; + private XstsConfigBuilder.InitPrec initPrec = XstsConfigBuilder.InitPrec.EMPTY; + private PruneStrategy pruneStrategy = PruneStrategy.LAZY; + private XstsConfigBuilder.OptimizeStmts optimizeStmts = XstsConfigBuilder.OptimizeStmts.ON; + private XstsConfigBuilder.AutoExpl autoExpl = XstsConfigBuilder.AutoExpl.NEWOPERANDS; + private ZoneRefinement zoneRefinement = ZoneRefinement.BW_ITP; + private TimedXstsActionProjections timedXstsActionProjections; + private ClockStrategy clockStrategy = ClockStrategy.NONE; + + public XstsCombinedConfigBuilder(final XstsConfigBuilder.Domain domain, final XstsConfigBuilder.Refinement refinement, final SolverFactory solverFactory) { + this.domain = domain; + this.refinement = refinement; + this.solverFactory = solverFactory; + } + + public XstsCombinedConfigBuilder logger(final Logger logger) { + this.logger = logger; + return this; + } + + public XstsCombinedConfigBuilder search(final Search search) { + this.search = search; + return this; + } + + public XstsCombinedConfigBuilder predSplit(final XstsConfigBuilder.PredSplit predSplit) { + this.predSplit = predSplit; + return this; + } + + public XstsCombinedConfigBuilder maxEnum(final int maxEnum) { + this.maxEnum = maxEnum; + return this; + } + + public XstsCombinedConfigBuilder initPrec(final XstsConfigBuilder.InitPrec initPrec) { + this.initPrec = initPrec; + return this; + } + + public XstsCombinedConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { + this.pruneStrategy = pruneStrategy; + return this; + } + + public XstsCombinedConfigBuilder optimizeStmts(final XstsConfigBuilder.OptimizeStmts optimizeStmts) { + this.optimizeStmts = optimizeStmts; + return this; + } + + public XstsCombinedConfigBuilder autoExpl(final XstsConfigBuilder.AutoExpl autoExpl) { + this.autoExpl = autoExpl; + return this; + } + + public XstsCombinedConfigBuilder zoneRefinement(final ZoneRefinement zoneRefinement) { + this.zoneRefinement = zoneRefinement; + return this; + } + + public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy) { + this.clockStrategy = clockStrategy; + return this; + } + + public XstsConfig build(XSTS xsts) { + final Solver abstractionSolver = solverFactory.createSolver(); + + timedXstsActionProjections = TimedXstsActionProjections.create(); + + xsts = clockStrategy.clockReplacer.apply(xsts); + + final Expr initFormula = xsts.getInitFormula(); + final Expr negProp = Not(xsts.getProp()); + + final Collection> clockVars = xsts.getVars().stream() + .filter(v -> v.getType() instanceof ClockType) + .map(v -> cast(v, Clock())) + .toList(); + final ZonePrec zonePrec = ZonePrec.of(clockVars); + final LazyStrategy lazyClockStrategy = createLazyZoneStrategy(zonePrec); + + final Lens lazyToConcrProd2Lens = XstsLazyLensUtils.createConcrProd2Lens(); + + final XstsCombinedExprTraceChecker traceChecker = createTraceChecker(initFormula, negProp, lazyToConcrProd2Lens); + final XstsCombinedPrecRefiner precRefiner = createPrecRefiner(xsts); + + final Refiner refiner; + if (refinement == XstsConfigBuilder.Refinement.MULTI_SEQ) { + refiner = MultiExprTraceRefiner.create(traceChecker, precRefiner, pruneStrategy, logger); + } else { + refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, pruneStrategy, logger); + } + + if (domain == XstsConfigBuilder.Domain.EXPL) { + + final LazyStrategy lazyDataStrategy = new BasicLazyStrategy<>( + XstsLazyLensUtils.createConcrDataLens(), + BasicConcretizer.create(ExplOrd.getInstance()) + ); + + final Function>, XstsState>>, ?> projection = s -> Tuple4.of( + s.getAbstrState().isInitialized(), + s.getAbstrState().lastActionWasEnv(), + lazyDataStrategy.getProjection().apply(s), + lazyClockStrategy.getProjection().apply(s) + ); + + final Prod2LazyStrategy lazyStrategy = new Prod2LazyStrategy<>(lazyToConcrProd2Lens, lazyDataStrategy, lazyClockStrategy, projection); + + final TimedXstsProd2Analysis splitProd2Analysis = TimedXstsProd2Analysis.create( + ExplStmtAnalysis.create(abstractionSolver, initFormula, maxEnum), + ZoneStmtAnalysis.getInstance(), + timedXstsActionProjections + ); + + final XstsAnalysis, Prod2Prec> xstsAnalysis = + XstsAnalysis.create(splitProd2Analysis); + + final LazyAnalysis lazyAnalysis = LazyAnalysis.create( + XstsOrd.create(lazyStrategy.getPartialOrd()), + xstsAnalysis.getInitFunc(), + xstsAnalysis.getTransFunc(), + XstsInitAbstractor.create(lazyStrategy.getInitAbstractor()) + ); + + final Predicate dataTarget = new ExplStatePredicate(negProp, abstractionSolver); + final Predicate> prod2Target = s -> dataTarget.test(s.getState1()); + final Predicate target = new XstsStatePredicate(prod2Target); + + final XstsStmtOptimizer> stmtOptimizer; + if (optimizeStmts == XstsConfigBuilder.OptimizeStmts.ON) { + stmtOptimizer = + XstsStmtOptimizer.create(Prod2StmtOptimizer.create( + ExplStmtOptimizer.getInstance(), + DefaultStmtOptimizer.create() + )); + } else { + stmtOptimizer = XstsStmtOptimizer.create(DefaultStmtOptimizer.create()); + } + + final Abstractor abstractor; + if (clockStrategy.controlFlowSplitting) { + final Solver cfSplitSolver = solverFactory.createSolver(); + final ValuationExtractor> valExtractor = + createDataValExtractor(ExplStateValuationExtractor.getInstance()); + final ControlFlowSplitXstsLts> lts = + ControlFlowSplitXstsLts.create(xsts, cfSplitSolver, valExtractor); + abstractor = new ControlFlowSplitLazyAbstractor(lts, search.strategy, lazyStrategy, lazyAnalysis, target, clockStrategy.filterInfeasibleCF); + } else { + final LTS>, XstsAction> lts = XstsLts.create(xsts, stmtOptimizer); + abstractor = new LazyAbstractor(lts, search.strategy, lazyStrategy, lazyAnalysis, target); + } + + final SafetyChecker>, XstsAction, Prod2Prec> + checker = CegarChecker.create(abstractor, refiner, logger); + final Prod2Prec prec = Prod2Prec.of(initPrec.builder.createExpl(xsts), zonePrec); + return XstsConfig.create(checker, prec); + + } else if (domain == XstsConfigBuilder.Domain.PRED_BOOL || domain == XstsConfigBuilder.Domain.PRED_CART || domain == XstsConfigBuilder.Domain.PRED_SPLIT) { + + final LazyStrategy lazyDataStrategy = new BasicLazyStrategy<>( + XstsLazyLensUtils.createConcrDataLens(), + BasicConcretizer.create(PredOrd.create(abstractionSolver)) + ); + + final Function>, XstsState>>, ?> projection = s -> Tuple4.of( + s.getAbstrState().isInitialized(), + s.getAbstrState().lastActionWasEnv(), + lazyDataStrategy.getProjection().apply(s), + lazyClockStrategy.getProjection().apply(s) + ); + + final Prod2LazyStrategy lazyStrategy = new Prod2LazyStrategy<>(lazyToConcrProd2Lens, lazyDataStrategy, lazyClockStrategy, projection); + + PredAbstractors.PredAbstractor predAbstractor = switch (domain) { + case PRED_BOOL -> PredAbstractors.booleanAbstractor(abstractionSolver); + case PRED_SPLIT -> PredAbstractors.booleanSplitAbstractor(abstractionSolver); + case PRED_CART -> PredAbstractors.cartesianAbstractor(abstractionSolver); + default -> throw new UnsupportedOperationException(domain + " domain is not supported."); + }; + + final TimedXstsProd2Analysis splitProd2Analysis = TimedXstsProd2Analysis.create( + PredAnalysis.create(abstractionSolver, predAbstractor, initFormula), + ZoneStmtAnalysis.getInstance(), + timedXstsActionProjections + ); + + final XstsAnalysis, Prod2Prec> xstsAnalysis = + XstsAnalysis.create(splitProd2Analysis); + + final LazyAnalysis lazyAnalysis = LazyAnalysis.create( + XstsOrd.create(lazyStrategy.getPartialOrd()), + xstsAnalysis.getInitFunc(), + xstsAnalysis.getTransFunc(), + XstsInitAbstractor.create(lazyStrategy.getInitAbstractor()) + ); + + final Predicate dataTarget = new ExprStatePredicate(negProp, abstractionSolver); + final Predicate> prod2Target = s -> dataTarget.test(s.getState1()); + final Predicate>> target = new XstsStatePredicate<>(prod2Target); + + final XstsStmtOptimizer> stmtOptimizer; + if (optimizeStmts == XstsConfigBuilder.OptimizeStmts.ON) { + stmtOptimizer = XstsStmtOptimizer.create(Prod2StmtOptimizer.create( + PredStmtOptimizer.getInstance(), + DefaultStmtOptimizer.create())); + } else { + stmtOptimizer = XstsStmtOptimizer.create(DefaultStmtOptimizer.create()); + } + + final Abstractor abstractor; + if (clockStrategy.controlFlowSplitting) { + final Solver cfSplitSolver = solverFactory.createSolver(); + final ValuationExtractor> valExtractor = + createDataValExtractor(PredStateValuationExtractor.getInstance()); + final ControlFlowSplitXstsLts> lts = + ControlFlowSplitXstsLts.create(xsts, cfSplitSolver, valExtractor); + abstractor = new ControlFlowSplitLazyAbstractor(lts, search.strategy, lazyStrategy, lazyAnalysis, target, clockStrategy.filterInfeasibleCF); + } else { + final LTS>, XstsAction> lts = XstsLts.create(xsts, stmtOptimizer); + abstractor = new LazyAbstractor<>(lts, search.strategy, lazyStrategy, lazyAnalysis, target); + } + + final SafetyChecker>, XstsAction, Prod2Prec> + checker = CegarChecker.create(abstractor, refiner, logger); + final Prod2Prec prec = Prod2Prec.of(initPrec.builder.createPred(xsts), zonePrec); + return XstsConfig.create(checker, prec); + + } else if (domain == XstsConfigBuilder.Domain.EXPL_PRED_BOOL || domain == XstsConfigBuilder.Domain.EXPL_PRED_CART || domain == XstsConfigBuilder.Domain.EXPL_PRED_COMBINED || domain == XstsConfigBuilder.Domain.EXPL_PRED_SPLIT) { + + final LazyStrategy lazyDataStrategy = new BasicLazyStrategy<>( + XstsLazyLensUtils.createConcrDataLens(), + BasicConcretizer.create(Prod2Ord.create(ExplOrd.getInstance(), PredOrd.create(abstractionSolver))) + ); + + final Function, ZoneState>>, XstsState, ZoneState>>>, ?> + projection = s -> Tuple4.of( + s.getAbstrState().isInitialized(), + s.getAbstrState().lastActionWasEnv(), + lazyDataStrategy.getProjection().apply(s), + lazyClockStrategy.getProjection().apply(s) + ); + + final Prod2LazyStrategy lazyStrategy = new Prod2LazyStrategy<>(lazyToConcrProd2Lens, lazyDataStrategy, lazyClockStrategy, projection); + + final Analysis, StmtAction, Prod2Prec> dataAnalysis; + + if (domain == XstsConfigBuilder.Domain.EXPL_PRED_BOOL || domain == XstsConfigBuilder.Domain.EXPL_PRED_CART || domain == XstsConfigBuilder.Domain.EXPL_PRED_SPLIT) { + final PredAbstractors.PredAbstractor predAbstractor = switch (domain) { + case EXPL_PRED_BOOL -> PredAbstractors.booleanAbstractor(abstractionSolver); + case EXPL_PRED_SPLIT -> PredAbstractors.booleanSplitAbstractor(abstractionSolver); + case EXPL_PRED_CART -> PredAbstractors.cartesianAbstractor(abstractionSolver); + default -> throw new UnsupportedOperationException(domain + " domain is not supported."); + }; + dataAnalysis = Prod2Analysis.create( + ExplStmtAnalysis.create(abstractionSolver, xsts.getInitFormula(), maxEnum), + PredAnalysis.create(abstractionSolver, predAbstractor, xsts.getInitFormula()), + Prod2ExplPredPreStrengtheningOperator.create(), + Prod2ExplPredStrengtheningOperator.create(abstractionSolver)); + } else { + final Prod2ExplPredAbstractors.Prod2ExplPredAbstractor prodAbstractor = Prod2ExplPredAbstractors.booleanAbstractor(abstractionSolver); + dataAnalysis = Prod2ExplPredAnalysis.create( + ExplAnalysis.create(abstractionSolver, xsts.getInitFormula()), + PredAnalysis.create(abstractionSolver, PredAbstractors.booleanAbstractor(abstractionSolver), xsts.getInitFormula()), + Prod2ExplPredStrengtheningOperator.create(abstractionSolver), + prodAbstractor); + } + + final TimedXstsProd2Analysis splitProd2Analysis = TimedXstsProd2Analysis.create( + dataAnalysis, ZoneStmtAnalysis.getInstance(), timedXstsActionProjections + ); + + final XstsAnalysis, ZoneState>, Prod2Prec, ZonePrec>> + xstsAnalysis = XstsAnalysis.create(splitProd2Analysis); + + final LazyAnalysis lazyAnalysis = LazyAnalysis.create( + XstsOrd.create(lazyStrategy.getPartialOrd()), + xstsAnalysis.getInitFunc(), + xstsAnalysis.getTransFunc(), + XstsInitAbstractor.create(lazyStrategy.getInitAbstractor()) + ); + + final Predicate dataTarget = new ExprStatePredicate(negProp, abstractionSolver); + final Predicate, ZoneState>> prod2Target = s -> dataTarget.test(s.getState1()); + final Predicate, ZoneState>>> target = new XstsStatePredicate<>(prod2Target); + + final XstsStmtOptimizer, ZoneState>> stmtOptimizer; + if (optimizeStmts == XstsConfigBuilder.OptimizeStmts.ON) { + stmtOptimizer = XstsStmtOptimizer.create(Prod2StmtOptimizer.create( + Prod2ExplPredStmtOptimizer.create(ExplStmtOptimizer.getInstance()), + DefaultStmtOptimizer.create())); + } else { + stmtOptimizer = XstsStmtOptimizer.create(DefaultStmtOptimizer.create()); + } + + final Abstractor abstractor; + if (clockStrategy.controlFlowSplitting) { + final Solver cfSplitSolver = solverFactory.createSolver(); + final ValuationExtractor, ZoneState>> valExtractor = + createDataValExtractor(Prod2ExplPredStateValuationExtractor.create(ExplStateValuationExtractor.getInstance())); + final ControlFlowSplitXstsLts, ZoneState>> lts = + ControlFlowSplitXstsLts.create(xsts, cfSplitSolver, valExtractor); + abstractor = new ControlFlowSplitLazyAbstractor(lts, search.strategy, lazyStrategy, lazyAnalysis, target, clockStrategy.filterInfeasibleCF); + } else { + final LTS, ZoneState>>, XstsAction> lts = + XstsLts.create(xsts, stmtOptimizer); + abstractor = new LazyAbstractor<>(lts, search.strategy, lazyStrategy, lazyAnalysis, target); + } + + final SafetyChecker, ZoneState>>, XstsAction, Prod2Prec, ZonePrec>> + checker = CegarChecker.create(abstractor, refiner, logger); + final Prod2Prec, ZonePrec> prec = Prod2Prec.of(initPrec.builder.createProd2ExplPred(xsts), zonePrec); + return XstsConfig.create(checker, prec); + + } else { + throw new UnsupportedOperationException(domain + " domain is not supported."); + } + } + + private ValuationExtractor> createDataValExtractor(final ValuationExtractor dataValExtractor) { + return new ValuationExtractor<>() { + @Override + public Valuation extractValuation(Prod2State state) { + return dataValExtractor.extractValuation(state.getState1()); + } + @Override + public Valuation extractValuationForVars(Prod2State state, Collection> vars) { + return dataValExtractor.extractValuationForVars(state.getState1(), vars); + } + }; + } + + private LazyStrategy>, XstsState>>, XstsAction> + createLazyZoneStrategy(final ZonePrec zonePrec) { + final Lens>, XstsState>>, LazyState> + lens = XstsLazyLensUtils.createLazyClockLens(); + final Lattice lattice = ZoneLattice.getInstance(); + final Interpolator interpolator = ZoneInterpolator.getInstance(); + final PartialOrd partialOrd = ZoneOrd.getInstance(); + final Concretizer concretizer = BasicConcretizer.create(partialOrd); + final InvTransFunc xstsZoneInvTransFunc = (state, action, prec) -> + ZoneStmtInvTransFunc.getInstance().getPreStates(state, timedXstsActionProjections.clockProjection(action), prec); + + switch (zoneRefinement) { + case BW_ITP: + return new BwItpStrategy<>(lens, lattice, interpolator, concretizer, xstsZoneInvTransFunc, zonePrec); + case FW_ITP: + final TransFunc xstsZoneTransFunc = (state, action, prec) -> + ZoneStmtTransFunc.getInstance().getSuccStates(state, timedXstsActionProjections.clockProjection(action), prec); + return new FwItpStrategy<>(lens, lattice, interpolator, concretizer, xstsZoneInvTransFunc, zonePrec, xstsZoneTransFunc, zonePrec); + default: + throw new AssertionError(); + } + } + + private XstsCombinedExprTraceChecker createTraceChecker(final Expr initFormula, final Expr negProp, + final Lens lens) { + final XstsCombinedExprTraceChecker traceChecker = new XstsCombinedExprTraceChecker( + switch (refinement) { + case FW_BIN_ITP -> ExprTraceFwBinItpChecker.create(initFormula, negProp, solverFactory.createItpSolver()); + case BW_BIN_ITP -> ExprTraceBwBinItpChecker.create(initFormula, negProp, solverFactory.createItpSolver()); + case SEQ_ITP, MULTI_SEQ -> ExprTraceSeqItpChecker.create(initFormula, negProp, solverFactory.createItpSolver()); + case UNSAT_CORE -> ExprTraceUnsatCoreChecker.create(initFormula, negProp, solverFactory.createUCSolver()); + }, lens, timedXstsActionProjections); + return traceChecker; + } + + private XstsCombinedPrecRefiner createPrecRefiner(final XSTS xsts) { + final XstsCombinedPrecRefiner precRefiner = new XstsCombinedPrecRefiner( + switch (domain) { + case EXPL -> new ItpRefToExplPrec(); + case PRED_BOOL, PRED_CART, PRED_SPLIT -> new ItpRefToPredPrec(predSplit.splitter); + case EXPL_PRED_BOOL, EXPL_PRED_CART, EXPL_PRED_COMBINED, EXPL_PRED_SPLIT -> + AutomaticItpRefToProd2ExplPredPrec.create(autoExpl.builder.create(xsts), predSplit.splitter); + }); + return precRefiner; + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedExprTraceChecker.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedExprTraceChecker.java new file mode 100644 index 0000000000..37c3ec7f4e --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedExprTraceChecker.java @@ -0,0 +1,43 @@ +package hu.bme.mit.theta.xsts.analysis.config.combined; + +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.lazy.LazyState; +import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceChecker; +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus; +import hu.bme.mit.theta.analysis.expr.refinement.Refutation; +import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.core.utils.Lens; +import hu.bme.mit.theta.xsts.analysis.XstsAction; +import hu.bme.mit.theta.xsts.analysis.XstsState; +import hu.bme.mit.theta.xsts.analysis.timed.TimedXstsActionProjections; + +public final class XstsCombinedExprTraceChecker implements ExprTraceChecker { + + private final ExprTraceChecker exprTraceChecker; + private final Lens>, XstsState>>, Prod2State> concrProd2Lens; + private final TimedXstsActionProjections timedXstsActionProjections; + + public XstsCombinedExprTraceChecker( + final ExprTraceChecker exprTraceChecker, + final Lens>, XstsState>>, Prod2State> concrProd2Lens, + final TimedXstsActionProjections timedXstsActionProjections) { + this.exprTraceChecker = exprTraceChecker; + this.concrProd2Lens = concrProd2Lens; + this.timedXstsActionProjections = timedXstsActionProjections; + } + + @Override + public ExprTraceStatus check(Trace trace) { + final Trace>, XstsState>>, XstsAction> + typedTrace = (Trace>, XstsState>>, XstsAction>) trace; + + final var newTrace = Trace.of( + typedTrace.getStates().stream().map(s -> concrProd2Lens.get(s).getState1()).toList(), + typedTrace.getActions().stream().map(timedXstsActionProjections::dataProjection).toList() + ); + + return exprTraceChecker.check(newTrace); + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedPrecRefiner.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedPrecRefiner.java new file mode 100644 index 0000000000..a9a51902ce --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedPrecRefiner.java @@ -0,0 +1,40 @@ +package hu.bme.mit.theta.xsts.analysis.config.combined; + +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.lazy.LazyState; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.expr.refinement.PrecRefiner; +import hu.bme.mit.theta.analysis.expr.refinement.Refutation; +import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; +import hu.bme.mit.theta.analysis.prod2.Prod2Prec; +import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.xsts.analysis.XstsAction; +import hu.bme.mit.theta.xsts.analysis.XstsState; + +import static com.google.common.base.Preconditions.checkNotNull; + +public final class XstsCombinedPrecRefiner + + implements PrecRefiner>, XstsState>>, XstsAction, Prod2Prec, R> { + + private final RefutationToPrec refToPrec; + + XstsCombinedPrecRefiner(final RefutationToPrec refToPrec) { + this.refToPrec = refToPrec; + } + + @Override + public Prod2Prec refine(Prod2Prec prec, Trace>, XstsState>>, XstsAction> trace, R refutation) { + checkNotNull(trace); + checkNotNull(prec); + checkNotNull(refutation); + DPrec runningPrec = prec.getPrec1(); + for (int i = 0; i < trace.getStates().size(); ++i) { + final DPrec precFromRef = refToPrec.toPrec(refutation, i); + runningPrec = refToPrec.join(runningPrec, precFromRef); + } + return Prod2Prec.of(runningPrec, prec.getPrec2()); + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsLazyLensUtils.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsLazyLensUtils.java new file mode 100644 index 0000000000..36b11ab7f9 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsLazyLensUtils.java @@ -0,0 +1,185 @@ +package hu.bme.mit.theta.xsts.analysis.config.combined; + +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.algorithm.lazy.LazyState; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.core.utils.Lens; +import hu.bme.mit.theta.xsts.analysis.XstsState; + +public final class XstsLazyLensUtils { + + public static Lens>, XstsState>>, LazyState> + createLazyDataLens() { + final Lens>, XstsState>>, DConcr> concrLens = createConcrDataLens(); + final Lens>, XstsState>>, DAbstr> abstrLens = createAbstrDataLens(); + return new Lens<>() { + @Override + public LazyState get(LazyState>, XstsState>> state) { + final DConcr concrState = concrLens.get(state); + if (concrState.isBottom()) { + return LazyState.bottom(concrState); + } else { + final DAbstr abstrState = abstrLens.get(state); + return LazyState.of(concrState, abstrState); + } + } + @Override + public LazyState>, XstsState>> set( + LazyState>, XstsState>> lazyState, + LazyState newItpDataState) { + final XstsState> newConcrState = concrLens.set(lazyState, newItpDataState.getConcrState()).getConcrState(); + final XstsState> newAbstrState = abstrLens.set(lazyState, newItpDataState.getAbstrState()).getAbstrState(); + return LazyState.of(newConcrState, newAbstrState); + } + }; + } + + public static Lens>, XstsState>>, LazyState> + createLazyClockLens() { + final Lens>, XstsState>>, CConcr> concrLens = createConcrClockLens(); + final Lens>, XstsState>>, CAbstr> abstrLens = createAbstrClockLens(); + return new Lens<>() { + @Override + public LazyState get(LazyState>, XstsState>> state) { + final CConcr concrState = concrLens.get(state); + if (concrState.isBottom()) { + return LazyState.bottom(concrState); + } else { + final CAbstr abstrState = abstrLens.get(state); + return LazyState.of(concrState, abstrState); + } + } + @Override + public LazyState>, XstsState>> set( + LazyState>, XstsState>> lazyState, + LazyState newItpDataState) { + final XstsState> newConcrState = concrLens.set(lazyState, newItpDataState.getConcrState()).getConcrState(); + final XstsState> newAbstrState = abstrLens.set(lazyState, newItpDataState.getAbstrState()).getAbstrState(); + return LazyState.of(newConcrState, newAbstrState); + } + }; + } + + public static Lens>, XstsState>>, DConcr> + createConcrDataLens() { + return new Lens<>() { + @Override + public DConcr get(LazyState>, XstsState>> state) { + return state.getConcrState().getState().getState1(); + } + @Override + public LazyState>, XstsState>> set( + LazyState>, XstsState>> lazyState, + DConcr newConcrDataState) { + final XstsState> concrXstsState = lazyState.getConcrState(); + final Prod2State concrState = concrXstsState.getState(); + final Prod2State newConcrState = concrState.with1(newConcrDataState); + final XstsState> newConcrXstsState = + XstsState.of(newConcrState, concrXstsState.lastActionWasEnv(), concrXstsState.isInitialized()); + return lazyState.withConcrState(newConcrXstsState); + } + }; + } + + public static Lens>, XstsState>>, DAbstr> + createAbstrDataLens() { + return new Lens<>() { + @Override + public DAbstr get(LazyState>, XstsState>> state) { + return state.getAbstrState().getState().getState1(); + } + @Override + public LazyState>, XstsState>> set( + LazyState>, XstsState>> lazyState, + DAbstr newAbstrDataState) { + final XstsState> abstrXstsState = lazyState.getAbstrState(); + final Prod2State abstrState = abstrXstsState.getState(); + final Prod2State newAbstrState = abstrState.with1(newAbstrDataState); + final XstsState> newAbstrXstsState = + XstsState.of(newAbstrState, abstrXstsState.lastActionWasEnv(), abstrXstsState.isInitialized()); + return lazyState.withAbstrState(newAbstrXstsState); + } + }; + } + + public static Lens>, XstsState>>, CConcr> + createConcrClockLens() { + return new Lens<>() { + @Override + public CConcr get(LazyState>, XstsState>> state) { + return state.getConcrState().getState().getState2(); + } + @Override + public LazyState>, XstsState>> set( + LazyState>, XstsState>> lazyState, + CConcr newConcrClockState) { + final XstsState> concrXstsState = lazyState.getConcrState(); + final Prod2State concrState = concrXstsState.getState(); + final Prod2State newConcrState = concrState.with2(newConcrClockState); + final XstsState> newConcrXstsState = + XstsState.of(newConcrState, concrXstsState.lastActionWasEnv(), concrXstsState.isInitialized()); + return lazyState.withConcrState(newConcrXstsState); + } + }; + } + + public static Lens>, XstsState>>, CAbstr> + createAbstrClockLens() { + return new Lens<>() { + @Override + public CAbstr get(LazyState>, XstsState>> state) { + return state.getAbstrState().getState().getState2(); + } + @Override + public LazyState>, XstsState>> set( + LazyState>, XstsState>> lazyState, + CAbstr newAbstrClockState) { + final XstsState> abstrXstsState = lazyState.getAbstrState(); + final Prod2State abstrState = abstrXstsState.getState(); + final Prod2State newAbstrState = abstrState.with2(newAbstrClockState); + final XstsState> newAbstrXstsState = + XstsState.of(newAbstrState, abstrXstsState.lastActionWasEnv(), abstrXstsState.isInitialized()); + return lazyState.withAbstrState(newAbstrXstsState); + } + }; + } + + public static Lens>, XstsState>>, Prod2State> + createConcrProd2Lens() { + return new Lens<>() { + @Override + public Prod2State get(LazyState>, XstsState>> state) { + return state.getConcrState().getState(); + } + @Override + public LazyState>, XstsState>> set( + LazyState>, XstsState>> lazyState, + Prod2State newConcrState) { + final XstsState> concrXstsState = lazyState.getConcrState(); + final XstsState> newXstsState = + XstsState.of(newConcrState, concrXstsState.lastActionWasEnv(), concrXstsState.isInitialized()); + return lazyState.withConcrState(newXstsState); + } + }; + } + + public static Lens>, XstsState>>, Prod2State> + createAbstrProd2Lens() { + return new Lens<>() { + @Override + public Prod2State get(LazyState>, XstsState>> state) { + return state.getAbstrState().getState(); + } + @Override + public LazyState>, XstsState>> set( + LazyState>, XstsState>> lazyState, + Prod2State newAbstrState) { + final XstsState> abstrXstsState = lazyState.getAbstrState(); + final XstsState> newXstsState = + XstsState.of(newAbstrState, abstrXstsState.lastActionWasEnv(), abstrXstsState.isInitialized()); + return lazyState.withAbstrState(newXstsState); + } + }; + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitLazyAbstractor.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitLazyAbstractor.java new file mode 100644 index 0000000000..fa4cafadf8 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitLazyAbstractor.java @@ -0,0 +1,207 @@ +package hu.bme.mit.theta.xsts.analysis.timed; + +import com.google.common.collect.Lists; +import hu.bme.mit.theta.analysis.*; +import hu.bme.mit.theta.analysis.algorithm.ARG; +import hu.bme.mit.theta.analysis.algorithm.ArgNode; +import hu.bme.mit.theta.analysis.algorithm.SearchStrategy; +import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor; +import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult; +import hu.bme.mit.theta.analysis.algorithm.lazy.LazyAnalysis; +import hu.bme.mit.theta.analysis.algorithm.lazy.LazyState; +import hu.bme.mit.theta.analysis.algorithm.lazy.LazyStatistics; +import hu.bme.mit.theta.analysis.algorithm.lazy.LazyStrategy; +import hu.bme.mit.theta.analysis.algorithm.runtimecheck.AbstractArg; +import hu.bme.mit.theta.analysis.algorithm.runtimecheck.ArgCexCheckHandler; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.reachedset.Partition; +import hu.bme.mit.theta.analysis.waitlist.Waitlist; +import hu.bme.mit.theta.xsts.analysis.XstsAction; +import hu.bme.mit.theta.xsts.analysis.XstsState; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Optional; +import java.util.function.Predicate; +import java.util.stream.Stream; + +import static com.google.common.base.Preconditions.checkNotNull; + +public final class ControlFlowSplitLazyAbstractor + implements Abstractor, XstsState>, XstsAction, P> { + + private final ControlFlowSplitXstsLts lts; + private final SearchStrategy searchStrategy; + private final LazyStrategy, XstsState>, XstsAction> lazyStrategy; + private final Analysis, XstsState>, XstsAction, P> analysis; + private final Predicate> isTarget; + private final boolean filterInfeasibleCF; + + public ControlFlowSplitLazyAbstractor(final ControlFlowSplitXstsLts lts, + final SearchStrategy searchStrategy, + final LazyStrategy, XstsState>, XstsAction> lazyStrategy, + final LazyAnalysis, XstsState, XstsAction, P> analysis, + final Predicate> isTarget, + final boolean filterInfeasibleCF) { + this.lts = checkNotNull(lts); + this.searchStrategy = checkNotNull(searchStrategy); + this.lazyStrategy = checkNotNull(lazyStrategy); + this.analysis = checkNotNull(analysis); + this.isTarget = isTarget; + this.filterInfeasibleCF = filterInfeasibleCF; + } + + @Override + public ARG, XstsState>, XstsAction> createArg() { + return ARG.create(analysis.getPartialOrd()); + } + + @Override + public AbstractorResult check(ARG, XstsState>, XstsAction> arg, P prec) { + Waitlist, XstsState>, XstsAction>> waiting = searchStrategy.createWaitlist(); + final Collection, XstsState>> + initStates = analysis.getInitFunc().getInitStates(prec); + if (arg.getInitNodes().count() < initStates.size()) { + for (final LazyState, XstsState> initState : initStates) { + final boolean target = isTarget.test(initState.getConcrState()); + arg.createInitNode(initState, target); + } + waiting.addAll(arg.getInitNodes()); + } else { + Stream, XstsState>, XstsAction>> incompleteNodes = arg.getIncompleteNodes(); + waiting.addAll(incompleteNodes); + } + ArgCexCheckHandler.instance.setCurrentArg(new AbstractArg<>(arg, prec)); + return new CheckMethod(arg, waiting, prec).run(); + } + + private final class CheckMethod { + final ARG, XstsState>, XstsAction> arg; + final P prec; + final LazyStatistics.Builder stats; + final Partition, XstsState>, XstsAction>, ?> passed; + final Waitlist, XstsState>, XstsAction>> waiting; + + public CheckMethod(final ARG, XstsState>, XstsAction> arg, + final Waitlist, XstsState>, XstsAction>> waiting, + final P prec) { + this.arg = arg; + this.prec = prec; + stats = LazyStatistics.builder(arg); + passed = Partition.of(n -> lazyStrategy.getProjection().apply(n.getState())); + this.waiting = waiting; + } + + public AbstractorResult run() { + stats.startAlgorithm(); + + if (arg.getInitNodes().anyMatch(ArgNode::isTarget)) { + return stop(AbstractorResult.unsafe()); + } + + while (!waiting.isEmpty()) { + final ArgNode, XstsState>, XstsAction> v = waiting.remove(); + assert v.isFeasible(); + + close(v, stats); + if (!v.isCovered()) { + AbstractorResult result = expand(v, arg, stats); + if (result.isUnsafe()) { + return stop(AbstractorResult.unsafe()); + } + } + ArgCexCheckHandler.instance.setCurrentArg(new AbstractArg<>(arg, prec)); + } + return stop(AbstractorResult.safe()); + } + + private AbstractorResult stop(AbstractorResult result) { + stats.stopAlgorithm(); + final LazyStatistics statistics = stats.build(); + return result; + } + + private void close(final ArgNode, XstsState>, XstsAction> coveree, + final LazyStatistics.Builder stats) { + stats.startClosing(); + + final Iterable, XstsState>, XstsAction>> + candidates = Lists.reverse(passed.get(coveree)); + for (final ArgNode, XstsState>, XstsAction> coverer : candidates) { + + stats.checkCoverage(); + if (lazyStrategy.mightCover(coveree, coverer)) { + + stats.attemptCoverage(); + + coveree.setCoveringNode(coverer); + final Collection, XstsState>, XstsAction>> + uncoveredNodes = new ArrayList<>(); + lazyStrategy.cover(coveree, coverer, uncoveredNodes); + waiting.addAll(uncoveredNodes.stream().filter(n -> !n.equals(coveree))); + + if (coveree.isCovered()) { + stats.successfulCoverage(); + stats.stopClosing(); + return; + } + } + } + + stats.stopClosing(); + } + + private AbstractorResult expand(final ArgNode, XstsState>, XstsAction> node, + final ARG, XstsState>, XstsAction> arg, + final LazyStatistics.Builder stats) { + stats.startExpanding(); + final LazyState, XstsState> state = node.getState(); + + lts.reset(); + lts.splitCF(state.getConcrState()); + if (filterInfeasibleCF) { + lts.filterCF(state.getAbstrState()); + } + Optional nextAction = lts.getNextEnabledAction(); + + while (nextAction.isPresent()) { + final XstsAction action = nextAction.get(); + + final Collection, XstsState>> + succStates = analysis.getTransFunc().getSuccStates(state, action, prec); + + for (final LazyState, XstsState> succState : succStates) { + if (node.getSuccNodes().noneMatch(n -> n.getInEdge().get().getAction().equals(action) + && n.getState().equals(succState))) { + if (lazyStrategy.inconsistentState(succState)) { + final Collection, XstsState>, XstsAction>> + uncoveredNodes = new ArrayList<>(); + lazyStrategy.disable(node, action, succState, uncoveredNodes); + waiting.addAll(uncoveredNodes); + + if (filterInfeasibleCF) { + lts.filterCF(node.getState().getAbstrState()); + } + } else { + final boolean target = isTarget.test(succState.getConcrState()); + final ArgNode, XstsState>, XstsAction> + succNode = arg.createSuccNode(node, action, succState, target); + if (target) { + stats.stopExpanding(); + return AbstractorResult.unsafe(); + } + waiting.add(succNode); + } + } + } + + nextAction = lts.getNextEnabledAction(); + } + + node.expanded = true; + passed.add(node); + stats.stopExpanding(); + return AbstractorResult.safe(); + } + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitResult.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitResult.java new file mode 100644 index 0000000000..81cfd24aac --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitResult.java @@ -0,0 +1,44 @@ +package hu.bme.mit.theta.xsts.analysis.timed; + +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.stmt.Stmt; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.utils.PathUtils; + +import java.util.Collection; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; + +public class ControlFlowSplitResult { + + private final Stmt flaggedStmt; + private final Collection> flags; + private final Expr indexedFlagConstraintExpr; + + + private ControlFlowSplitResult(final Stmt flaggedStmt, final Collection> flags, + final Collection> flagConstraints) { + + this.flaggedStmt = flaggedStmt; + this.flags = flags; + this.indexedFlagConstraintExpr = PathUtils.unfold(And(flagConstraints), 0); + } + + public static ControlFlowSplitResult of(final Stmt flaggedStmt, final Collection> flags, + final Collection> flagConstraints) { + return new ControlFlowSplitResult(flaggedStmt, flags, flagConstraints); + } + + public Stmt getFlaggedStmt() { + return flaggedStmt; + } + + public Collection> getFlags() { + return flags; + } + + public Expr getIndexedFlagConstraintExpr() { + return indexedFlagConstraintExpr; + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitUtil.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitUtil.java new file mode 100644 index 0000000000..f9fa0a6c50 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitUtil.java @@ -0,0 +1,370 @@ +package hu.bme.mit.theta.xsts.analysis.timed; + +import com.google.common.collect.Lists; +import hu.bme.mit.theta.core.decl.ParamDecl; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.stmt.IfStmt; +import hu.bme.mit.theta.core.stmt.NonDetStmt; +import hu.bme.mit.theta.core.stmt.SequenceStmt; +import hu.bme.mit.theta.core.stmt.*; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.booltype.*; +import hu.bme.mit.theta.core.type.clocktype.ClockConstraintExpr; +import hu.bme.mit.theta.core.type.clocktype.ClockExprs; +import hu.bme.mit.theta.core.type.clocktype.ClockType; +import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.core.utils.*; + +import java.util.*; + +import static hu.bme.mit.theta.core.stmt.Stmts.*; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static java.util.stream.Collectors.toList; + +public class ControlFlowSplitUtil { + + private ControlFlowSplitUtil() { + } + + public static ControlFlowSplitResult splitCF(final Stmt stmt) { + + final List> flags = new ArrayList<>(); + final List> flagConstraints = new ArrayList<>(); + + final ControlFlowFlagsHelper helper = new ControlFlowFlagsHelper(flags, flagConstraints); + final Stmt flaggedStmt = helper.flagStmt(stmt); + + for (final VarDecl flag : Lists.reverse(flags)) { + VarPoolUtil.returnBool(flag); + } + + return ControlFlowSplitResult.of(flaggedStmt, flags, flagConstraints); + } + + private static final class ControlFlowFlagsHelper implements StmtVisitor, Stmt> { + + private final List> flags; + private final List> flagConstraints; + private final AssumeTransformationHelper assumeHelper; + + private ControlFlowFlagsHelper(final List> flags, final List> flagConstraints) { + this.flags = flags; + this.flagConstraints = flagConstraints; + assumeHelper = new AssumeTransformationHelper(); + } + + public Stmt flagStmt(final Stmt stmt) { + final VarDecl root = VarPoolUtil.requestBool(); + flags.add(root); + flagConstraints.add(root.getRef()); + + final Stmt flaggedStmt = stmt.accept(this, root); + final AssumeStmt flagConstraintsAssume = Stmts.Assume(And(flagConstraints)); + + return Stmts.SequenceStmt(List.of(flaggedStmt, flagConstraintsAssume)); + } + + @Override + public Stmt visit(SkipStmt stmt, VarDecl parent) { + return stmt; + } + + @Override + public Stmt visit(AssumeStmt stmt, VarDecl parent) { + if (!stmt.accept(StmtContainsTimingVisitor.getInstance(), null)) { + return stmt; + } + return assumeHelper.transformAssume(stmt.getCond(), parent); + } + + @Override + public Stmt visit(AssignStmt stmt, VarDecl parent) { + final VarDecl varDecl = stmt.getVarDecl(); + + if (!(varDecl.getType() instanceof BoolType) || !stmt.accept(StmtContainsTimingVisitor.getInstance(), null)) { + return stmt; + } + + final Expr assignExpr = stmt.getExpr(); + final Expr cond = TypeUtils.cast(assignExpr, Bool()); + final VarDecl boolVarDecl = TypeUtils.cast(varDecl, Bool()); + final AssignStmt then = Assign(boolVarDecl, True()); + final AssignStmt elze = Assign(boolVarDecl, False()); + + final IfStmt assignToIfStmt = IfStmt(cond, then, elze); + return assignToIfStmt.accept(this, parent); + } + + @Override + public Stmt visit(HavocStmt stmt, VarDecl parent) { + return stmt; + } + + @Override + public Stmt visit(SequenceStmt stmt, VarDecl parent) { + final List flaggedSubStmts = stmt.getStmts().stream() + .map(subStmt -> subStmt.accept(this, parent)) + .toList(); + return SequenceStmt(flaggedSubStmts); + } + + @Override + public Stmt visit(NonDetStmt stmt, VarDecl parent) { + if (!stmt.accept(StmtContainsTimingVisitor.getInstance(), null)) { + return stmt; + } + + final List branches = stmt.getStmts(); + final int branchCnt = branches.size(); + + if (branchCnt == 1) { + return branches.get(0).accept(this, parent); + } + + final List> localFlags = new ArrayList<>(branchCnt); + final List flaggedBranches = new ArrayList<>(branchCnt); + + for (final Stmt branch : branches) { + final VarDecl flag = VarPoolUtil.requestBool(); + localFlags.add(flag); + flags.add(flag); + flagConstraints.add(Imply(Not(parent.getRef()), Not(flag.getRef()))); + + final Stmt flaggedBranchBody = branch.accept(this, flag); + final IfStmt flaggedBranch = IfStmt(flag.getRef(), flaggedBranchBody); + flaggedBranches.add(flaggedBranch); + } + + final List> branchExprs = new ArrayList<>(); + for (int i = 0; i < localFlags.size(); i++) { + final List> flagsForCurrentBranch = new ArrayList<>(); + for (int j = 0; j < localFlags.size(); j++) { + final RefExpr flagExpr = localFlags.get(j).getRef(); + flagsForCurrentBranch.add((i == j) ? flagExpr : Not(flagExpr)); + } + branchExprs.add(And(flagsForCurrentBranch)); + } + flagConstraints.add(Imply(parent.getRef(), Or(branchExprs))); + + return SequenceStmt(flaggedBranches); + } + + @Override + public Stmt visit(OrtStmt stmt, VarDecl parent) { + throw new UnsupportedOperationException(); + } + + @Override + public Stmt visit(LoopStmt stmt, VarDecl parent) { + throw new UnsupportedOperationException(); + } + + @Override + public Stmt visit(IfStmt stmt, VarDecl parent) { + if (!stmt.accept(StmtContainsTimingVisitor.getInstance(), null)) { + return stmt; + } + + final Map, Stmt> condToBranch = new LinkedHashMap<>(2, 1); + condToBranch.put(stmt.getCond(), stmt.getThen()); + condToBranch.put(Not(stmt.getCond()), stmt.getElze()); + + final List> localFlags = new ArrayList<>(2); + final List flaggedBranches = new ArrayList<>(2); + + for (final Map.Entry, Stmt> branch : condToBranch.entrySet()) { + final VarDecl flag = VarPoolUtil.requestBool(); + localFlags.add(flag); + flags.add(flag); + + final Expr cond = branch.getKey(); + final Stmt branchBody = branch.getValue(); + final Stmt newBranchBody = SequenceStmt(List.of(Assume(cond), branchBody)); + final Stmt flaggedBranchBody = newBranchBody.accept(this, flag); + + final IfStmt flaggedBranch = IfStmt(flag.getRef(), flaggedBranchBody); + flaggedBranches.add(flaggedBranch); + } + + final Expr p = parent.getRef(); + final Expr b1 = localFlags.get(0).getRef(); + final Expr b2 = localFlags.get(1).getRef(); + flagConstraints.add(Imply(p, Xor(b1, b2))); + flagConstraints.add(Imply(Not(p), Not(b1))); + flagConstraints.add(Imply(Not(p), Not(b2))); + + return SequenceStmt(flaggedBranches); + } + + @Override + public Stmt visit(DelayStmt stmt, VarDecl parent) { + return stmt; + } + + @Override + public Stmt visit(ResetStmt stmt, VarDecl parent) { + return stmt; + } + + + private final class AssumeTransformationHelper { + + private AssumeTransformationHelper() { + } + + private Stmt transformAssume(final Expr cond, final VarDecl parent) { + if (cond instanceof NotExpr) { + return transformNot((NotExpr) cond, parent); + } else if (cond instanceof AndExpr) { + return transformAnd((AndExpr) cond, parent); + } else if (cond instanceof OrExpr) { + return transformOr((OrExpr) cond, parent); + } else if (cond instanceof ImplyExpr) { + return transformImply((ImplyExpr) cond, parent); + } else if (cond instanceof IffExpr) { + return transformIff((IffExpr) cond, parent); + } else if (cond instanceof XorExpr) { + return transformXor((XorExpr) cond, parent); + } else if (cond instanceof QuantifiedExpr) { + throw new UnsupportedOperationException(); + } else { + return Assume(cond); + } + } + + private Stmt transformAnd(final AndExpr andExpr, final VarDecl parent) { + final List assumes = andExpr.getOps().stream().map(Stmts::Assume).collect(toList()); + final Stmt transformed = SequenceStmt(assumes); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformOr(final OrExpr orExpr, final VarDecl parent) { + final List assumes = orExpr.getOps().stream().map(Stmts::Assume).collect(toList()); + final Stmt transformed = NonDetStmt(assumes); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformImply(final ImplyExpr implyExpr, final VarDecl parent) { + final Expr a = implyExpr.getLeftOp(); + final Expr b = implyExpr.getRightOp(); + final Stmt transformed = Assume(Or(Not(a), b)); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformIff(final IffExpr iffExpr, final VarDecl parent) { + final Expr a = iffExpr.getLeftOp(); + final Expr b = iffExpr.getRightOp(); + final Expr imply1 = Or(Not(a), b); + final Expr imply2 = Or(Not(b), a); + final Stmt transformed = Assume(And(imply1, imply2)); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformXor(final XorExpr xorExpr, final VarDecl parent) { + final Expr a = xorExpr.getLeftOp(); + final Expr b = xorExpr.getRightOp(); + final Expr case1 = And(Not(a), b); + final Expr case2 = And(a, Not(b)); + final Stmt transformed = Assume(Or(case1, case2)); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformNot(final NotExpr notExpr, final VarDecl parent) { + final Expr op = notExpr.getOp(); + if (op instanceof ClockConstraintExpr) { + return transformNegatedClockConstraint((ClockConstraintExpr) op); + } else if (op instanceof NotExpr) { + return transformNegatedNot((NotExpr) op, parent); + } else if (op instanceof AndExpr) { + return transformNegatedAnd((AndExpr) op, parent); + } else if (op instanceof OrExpr) { + return transformNegatedOr((OrExpr) op, parent); + } else if (op instanceof ImplyExpr) { + return transformNegatedImply((ImplyExpr) op, parent); + } else if (op instanceof IffExpr) { + return transformNegatedIff((IffExpr) op, parent); + } else if (op instanceof XorExpr) { + return transformNegatedXor((XorExpr) op, parent); + } else if (op instanceof ExistsExpr) { + return transformNegatedExists((ExistsExpr) op, parent); + } else if (op instanceof ForallExpr) { + return transformNegatedForall((ForallExpr) op, parent); + } else { + return Assume(notExpr); + } + } + + private Stmt transformNegatedClockConstraint(final ClockConstraintExpr negatedClockConstraint) { + final Expr clock = negatedClockConstraint.getLeftOp(); + final Expr value = negatedClockConstraint.getRightOp(); + final ClockConstraintExpr complement = switch (negatedClockConstraint.getRel()) { + case LT -> ClockExprs.Geq(clock, value); + case LEQ -> ClockExprs.Gt(clock, value); + case GT -> ClockExprs.Leq(clock, value); + case GEQ -> ClockExprs.Lt(clock, value); + default -> throw new UnsupportedOperationException(); + }; + return Assume(complement); + } + + private Stmt transformNegatedNot(final NotExpr negatedNotExpr, final VarDecl parent) { + final Stmt transformed = Assume(negatedNotExpr.getOp()); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformNegatedAnd(final AndExpr negatedAndExpr, final VarDecl parent) { + final List negatedOps = negatedAndExpr.getOps().stream().map(BoolExprs::Not).toList(); + final Stmt transformed = Assume(Or(negatedOps)); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformNegatedOr(final OrExpr negatedOrExpr, final VarDecl parent) { + final List negatedOps = negatedOrExpr.getOps().stream().map(BoolExprs::Not).toList(); + final Stmt transformed = Assume(And(negatedOps)); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformNegatedImply(final ImplyExpr negatedImplyExpr, final VarDecl parent) { + final Expr a = negatedImplyExpr.getLeftOp(); + final Expr b = negatedImplyExpr.getRightOp(); + final Stmt transformed = Assume(And(a, Not(b))); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformNegatedIff(final IffExpr negatedIffExpr, final VarDecl parent) { + final Expr a = negatedIffExpr.getLeftOp(); + final Expr b = negatedIffExpr.getRightOp(); + final Expr notImply1 = And(a, Not(b)); + final Expr notImply2 = And(b, Not(a)); + final Stmt transformed = Assume(Or(notImply1, notImply2)); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformNegatedXor(final XorExpr negatedXorExpr, final VarDecl parent) { + final Expr a = negatedXorExpr.getLeftOp(); + final Expr b = negatedXorExpr.getRightOp(); + final Expr same1 = And(a, b); + final Expr same2 = And(Not(a), Not(b)); + final Stmt transformed = Assume(Or(same1, same2)); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformNegatedExists(final ExistsExpr negatedExistsExpr, final VarDecl parent) { + final List> params = negatedExistsExpr.getParamDecls(); + final Expr op = negatedExistsExpr.getOp(); + final Stmt transformed = Assume(Forall(params, Not(op))); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + + private Stmt transformNegatedForall(final ForallExpr negatedForallExpr, final VarDecl parent) { + final List> params = negatedForallExpr.getParamDecls(); + final Expr op = negatedForallExpr.getOp(); + final Stmt transformed = Assume(Exists(params, Not(op))); + return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + } + } + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitXstsLts.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitXstsLts.java new file mode 100644 index 0000000000..e3c0a39782 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitXstsLts.java @@ -0,0 +1,165 @@ +package hu.bme.mit.theta.xsts.analysis.timed; + +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.stmtoptimizer.StmtSimplifier; +import hu.bme.mit.theta.analysis.utils.ValuationExtractor; +import hu.bme.mit.theta.core.clock.impl.RatClockImpl; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.stmt.NonDetStmt; +import hu.bme.mit.theta.core.stmt.Stmt; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; +import hu.bme.mit.theta.core.utils.PathUtils; +import hu.bme.mit.theta.core.utils.StmtUtils; +import hu.bme.mit.theta.core.utils.TypeUtils; +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.XstsAction; +import hu.bme.mit.theta.xsts.analysis.XstsState; + +import java.util.*; +import java.util.function.Function; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Clock; + +public class ControlFlowSplitXstsLts implements LTS, XstsAction> { + + private final Solver solver; + private final ValuationExtractor valExtractor; + + private final NonDetStmt init; + private final NonDetStmt tran; + private final NonDetStmt env; + private final Set> ctrlVars; + + private final Function stmtClockTransformer; + private final Map cfSplitCache; + + private ControlFlowSplitResult cfSplitResult; + private ExprState lastState; + private boolean stmtInSolver; + + private ControlFlowSplitXstsLts(final XSTS xsts, final Solver solver, final ValuationExtractor valExtractor) { + this.solver = solver; + this.valExtractor = valExtractor; + + init = xsts.getInit(); + tran = xsts.getTran(); + env = xsts.getEnv(); + ctrlVars = xsts.getCtrlVars(); + + final List> clocks = xsts.getVars().stream() + .filter(varDecl -> varDecl.getType() instanceof ClockType) + .map(varDecl -> TypeUtils.cast(varDecl, Clock())) + .toList(); + if (clocks.isEmpty()) { + stmtClockTransformer = stmt -> stmt; + } else { + stmtClockTransformer = RatClockImpl.fromClocks(clocks)::transformStmt; + } + cfSplitCache = new HashMap<>(); + } + + public static ControlFlowSplitXstsLts create(final XSTS xsts, final Solver solver, + final ValuationExtractor valExtractor) { + return new ControlFlowSplitXstsLts<>(xsts, solver, valExtractor); + } + + @Override + public Collection getEnabledActionsFor(XstsState state) { + reset(); + splitCF(state); + return getEnabledActions(); + } + + public Collection getEnabledActionsFor(XstsState state, ExprState abstrState) { + reset(); + splitCF(state); + filterCF(abstrState); + return getEnabledActions(); + } + + public void reset() { + if (!solver.getAssertions().isEmpty()) { + solver.pop(); + } + lastState = null; + stmtInSolver = false; + } + + public void splitCF(final XstsState state) { + final Stmt xstsStep; + if (!state.isInitialized()) xstsStep = init; + else if (state.lastActionWasEnv()) xstsStep = tran; + else xstsStep = env; + + final Valuation ctrlVal = valExtractor.extractValuationForVars(state.getState(), ctrlVars); + final Stmt simplifiedStmt = StmtSimplifier.simplifyStmt(ctrlVal, xstsStep); + cfSplitResult = cfSplitCache.computeIfAbsent(simplifiedStmt, ControlFlowSplitUtil::splitCF); + + solver.push(); + solver.add(cfSplitResult.getIndexedFlagConstraintExpr()); + } + + public void filterCF(final ExprState state) { + if (state != lastState) { + solver.add(PathUtils.unfold(state.toExpr(), 0)); + } + if (!stmtInSolver) { + final Stmt stmtWithoutClocks = stmtClockTransformer.apply(cfSplitResult.getFlaggedStmt()); + StmtUtils.toExpr(stmtWithoutClocks, VarIndexingFactory.indexing(0)).getExprs() + .forEach(expr -> solver.add(PathUtils.unfold(expr, 0))); + stmtInSolver = true; + } + } + + public Optional getNextEnabledAction() { + if (solver.getAssertions().isEmpty()) { + throw new IllegalStateException(); + } + + final SolverStatus status = solver.check(); + if (status.isSat()) { + final Valuation model = solver.getModel(); + final Collection> flags = cfSplitResult.getFlags(); + final Valuation flagsVal = PathUtils.extractValuation(model, 0, flags); + + final List> negatedFlags = new ArrayList<>(); + for (final VarDecl flag : flags) { + final Optional> flagValue = flagsVal.eval(flag); + if (flagValue.isPresent()) { + final BoolLitExpr boolValue = (BoolLitExpr) flagValue.get(); + negatedFlags.add(boolValue.getValue() ? Not(flag.getRef()) : flag.getRef()); + } + } + solver.add(PathUtils.unfold(Or(negatedFlags), 0)); + + final Stmt flaggedStmt = cfSplitResult.getFlaggedStmt(); + final Stmt resultStmt = StmtSimplifier.simplifyStmt(flagsVal, flaggedStmt); + final XstsAction action = XstsAction.create(resultStmt); + + return Optional.of(action); + + } else { + return Optional.empty(); + } + } + + private Collection getEnabledActions() { + final List actions = new ArrayList<>(); + Optional action = getNextEnabledAction(); + while (action.isPresent()) { + actions.add(action.get()); + action = getNextEnabledAction(); + } + return actions; + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/TimedXstsActionProjections.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/TimedXstsActionProjections.java new file mode 100644 index 0000000000..1ee0f929b5 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/TimedXstsActionProjections.java @@ -0,0 +1,166 @@ +package hu.bme.mit.theta.xsts.analysis.timed; + +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.stmt.*; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.clocktype.ClockType; +import hu.bme.mit.theta.core.utils.ExprUtils; +import hu.bme.mit.theta.core.utils.StmtContainsTimingVisitor; +import hu.bme.mit.theta.xsts.analysis.XstsAction; + +import java.util.*; + +import static hu.bme.mit.theta.core.stmt.Stmts.Assume; + +public class TimedXstsActionProjections { + + private final Map dataProjections; + private final Map clockProjections; + + private TimedXstsActionProjections() { + dataProjections = new HashMap<>(); + clockProjections = new HashMap<>(); + } + + public static TimedXstsActionProjections create() { + return new TimedXstsActionProjections(); + } + + public XstsAction dataProjection(final XstsAction action) { + XstsAction dataAction = dataProjections.get(action); + if (dataAction == null) { + createProjections(action); + dataAction = dataProjections.get(action); + } + return dataAction; + } + + public XstsAction clockProjection(final XstsAction action) { + XstsAction clockAction = clockProjections.get(action); + if (clockAction == null) { + createProjections(action); + clockAction = clockProjections.get(action); + } + return clockAction; + } + + private void createProjections(final XstsAction action) { + final List dataStmts = new ArrayList<>(); + final List clockStmts = new ArrayList<>(); + final Tuple2, List> projections = Tuple2.of(dataStmts, clockStmts); + + for (final Stmt stmt : action.getStmts()) { + stmt.accept(new ProjectionVisitor(), projections); + } + + final XstsAction dataAction = XstsAction.create(projections.get1()); + dataProjections.put(action, dataAction); + + final XstsAction clockAction = XstsAction.create(projections.get2()); + clockProjections.put(action, clockAction); + } + + private static class ProjectionVisitor implements StmtVisitor, List>, Void> { + + @Override + public Void visit(SkipStmt stmt, Tuple2, List> projections) { + return null; + } + + @Override + public Void visit(AssumeStmt stmt, Tuple2, List> projections) { + for (final Expr cond : ExprUtils.getConjuncts(stmt.getCond())) { + final Collection> vars = ExprUtils.getVars(cond); + final long varsCnt = vars.size(); + final long clocksCnt = vars.stream().filter(v -> v.getType() instanceof ClockType).count(); + if (clocksCnt == 0) { + addDataStmt(Assume(cond), projections); + } else if (clocksCnt == varsCnt) { + addClockStmt(Assume(cond), projections); + } else { + throw new AssertionError(); + } + } + return null; + } + + @Override + public Void visit(AssignStmt stmt, Tuple2, List> projections) { + shouldNotContainClock(stmt); + addDataStmt(stmt, projections); + return null; + } + + @Override + public Void visit(HavocStmt stmt, Tuple2, List> projections) { + shouldNotContainClock(stmt); + addDataStmt(stmt, projections); + return null; + } + + @Override + public Void visit(SequenceStmt stmt, Tuple2, List> projections) { + stmt.getStmts().forEach(subStmt -> subStmt.accept(this, projections)); + return null; + } + + @Override + public Void visit(NonDetStmt stmt, Tuple2, List> projections) { + if (stmt.getStmts().size() > 1) { + shouldNotContainClock(stmt); + } + addDataStmt(stmt, projections); + return null; + } + + @Override + public Void visit(OrtStmt stmt, Tuple2, List> projections) { + shouldNotContainClock(stmt); + addDataStmt(stmt, projections); + return null; + } + + @Override + public Void visit(LoopStmt stmt, Tuple2, List> projections) { + shouldNotContainClock(stmt); + addDataStmt(stmt, projections); + return null; + } + + @Override + public Void visit(IfStmt stmt, Tuple2, List> projections) { + shouldNotContainClock(stmt); + addDataStmt(stmt, projections); + return null; + } + + @Override + public Void visit(DelayStmt stmt, Tuple2, List> projections) { + addClockStmt(stmt, projections); + return null; + } + + @Override + public Void visit(ResetStmt stmt, Tuple2, List> projections) { + addClockStmt(stmt, projections); + return null; + } + + private void addDataStmt(final Stmt dataStmt, final Tuple2, List> projections) { + projections.get1().add(dataStmt); + } + + private void addClockStmt(final Stmt clockStmt, final Tuple2, List> projections) { + projections.get2().add(clockStmt); + } + + private static void shouldNotContainClock(final Stmt stmt) { + if (stmt.accept(StmtContainsTimingVisitor.getInstance(), null)) { + throw new AssertionError(); + } + } + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/TimedXstsProd2Analysis.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/TimedXstsProd2Analysis.java new file mode 100644 index 0000000000..74b0de33e7 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/TimedXstsProd2Analysis.java @@ -0,0 +1,62 @@ +package hu.bme.mit.theta.xsts.analysis.timed; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.InitFunc; +import hu.bme.mit.theta.analysis.PartialOrd; +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.TransFunc; +import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.analysis.prod2.Prod2InitFunc; +import hu.bme.mit.theta.analysis.prod2.Prod2Ord; +import hu.bme.mit.theta.analysis.prod2.Prod2Prec; +import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.analysis.prod2.Prod2TransFunc; +import hu.bme.mit.theta.xsts.analysis.XstsAction; + +import static com.google.common.base.Preconditions.checkNotNull; + +public final class TimedXstsProd2Analysis + implements Analysis, XstsAction, Prod2Prec> { + + private final PartialOrd> partialOrd; + private final InitFunc, Prod2Prec> initFunc; + private final TransFunc, XstsAction, Prod2Prec> transFunc; + + private TimedXstsProd2Analysis(final Analysis dataAnalysis, + final Analysis clockAnalysis, + final TimedXstsActionProjections actionProjections) { + checkNotNull(dataAnalysis); + checkNotNull(clockAnalysis); + this.partialOrd = Prod2Ord.create(dataAnalysis.getPartialOrd(), clockAnalysis.getPartialOrd()); + this.initFunc = Prod2InitFunc.create(dataAnalysis.getInitFunc(), clockAnalysis.getInitFunc()); + + final TransFunc dataTransFunc = (state, action, prec) + -> dataAnalysis.getTransFunc().getSuccStates(state, actionProjections.dataProjection(action), prec); + final TransFunc clockTransFunc = (state, action, prec) + -> clockAnalysis.getTransFunc().getSuccStates(state, actionProjections.clockProjection(action), prec); + this.transFunc = Prod2TransFunc.create(dataTransFunc, clockTransFunc); + } + + public static TimedXstsProd2Analysis create( + final Analysis dataAnalysis, + final Analysis clockAnalysis, + final TimedXstsActionProjections actionSplitter) { + return new TimedXstsProd2Analysis<>(dataAnalysis, clockAnalysis, actionSplitter); + } + + @Override + public PartialOrd> getPartialOrd() { + return partialOrd; + } + + @Override + public InitFunc, Prod2Prec> getInitFunc() { + return initFunc; + } + + @Override + public TransFunc, XstsAction, Prod2Prec> getTransFunc() { + return transFunc; + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/clocks/XstsClockReplacers.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/XstsClockReplacers.java similarity index 92% rename from subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/clocks/XstsClockReplacers.java rename to subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/XstsClockReplacers.java index d422a51259..09e6673b2a 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/clocks/XstsClockReplacers.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/XstsClockReplacers.java @@ -1,26 +1,21 @@ -package hu.bme.mit.theta.xsts.analysis.clocks; +package hu.bme.mit.theta.xsts.analysis.timed; import hu.bme.mit.theta.core.clock.impl.*; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.NonDetStmt; import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.abstracttype.EqExpr; import hu.bme.mit.theta.core.type.abstracttype.Ordered; import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.clocktype.ClockEqExpr; import hu.bme.mit.theta.core.type.clocktype.ClockExprs; import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.core.type.inttype.IntExprs; -import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.type.XstsPrimitiveType; import hu.bme.mit.theta.xsts.type.XstsType; import java.util.Collection; -import java.util.List; import java.util.Map; import java.util.function.Function; -import java.util.stream.Stream; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; import static hu.bme.mit.theta.core.type.clocktype.ClockExprs.Clock; diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsCFSplitCombinedAlgTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsCFSplitCombinedAlgTest.java new file mode 100644 index 0000000000..f3aea5d6cd --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsCFSplitCombinedAlgTest.java @@ -0,0 +1,127 @@ +package hu.bme.mit.theta.xsts.analysis; + +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; +import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; +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.analysis.config.combined.XstsCombinedConfigBuilder; +import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.*; +import java.util.Arrays; +import java.util.Collection; + +import static org.junit.Assert.assertTrue; + +@RunWith(value = Parameterized.class) +public class TimedXstsCFSplitCombinedAlgTest { + + @Parameterized.Parameter(value = 0) + public String filePath; + + @Parameterized.Parameter(value = 1) + public String propPath; + + @Parameterized.Parameter(value = 2) + public boolean safe; + + @Parameterized.Parameter(value = 3) + public XstsConfigBuilder.Domain domain; + + @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}, {3}") + public static Collection data() { + return Arrays.asList(new Object[][] { + + { "src/test/resources/model/Crossroad-Theta_timed.xsts", "src/test/resources/property/crossroad_safety.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/Crossroad-Theta_timed.xsts", "src/test/resources/property/crossroad_safety.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival1.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival1.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival2.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival2.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival3.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival3.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival4.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival4.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival5.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival5.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival6.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival6.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival7.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival7.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival8.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival8.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival9.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival9.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival10.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival10.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/clocks.xsts", "src/test/resources/property/clocks.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/clocks.xsts", "src/test/resources/property/clocks.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/xta_to_txsts.xsts", "src/test/resources/property/xta_to_txsts.prop", true, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/xta_to_txsts.xsts", "src/test/resources/property/xta_to_txsts.prop", true, XstsConfigBuilder.Domain.PRED_CART}, + + { "src/test/resources/model/xta_to_txsts.xsts", "src/test/resources/property/xta_to_txsts.prop", true, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + }); + } + + @Test + public void test() throws IOException { + + final Logger logger = new ConsoleLogger(Level.SUBSTEP); + + XSTS xsts; + try (InputStream inputStream = new SequenceInputStream(new FileInputStream(filePath), new FileInputStream(propPath))) { + xsts = XstsDslManager.createXsts(inputStream); + } + + final XstsConfig configuration = new XstsCombinedConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()) + .initPrec(XstsConfigBuilder.InitPrec.CTRL) + .optimizeStmts(XstsConfigBuilder.OptimizeStmts.ON) + .predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS) + .maxEnum(250) + .pruneStrategy(PruneStrategy.FULL) + .clockStrategy(XstsCombinedConfigBuilder.ClockStrategy.CF_SPLIT_ALL) + .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/TimedXstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsTest.java new file mode 100644 index 0000000000..9d72d4806b --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsTest.java @@ -0,0 +1,116 @@ +package hu.bme.mit.theta.xsts.analysis; + +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; +import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; +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 org.junit.runner.RunWith; +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; +import java.util.Collection; + +import static org.junit.Assert.assertTrue; + +@RunWith(value = Parameterized.class) +public class TimedXstsTest { + + @Parameterized.Parameter(value = 0) + public String filePath; + + @Parameterized.Parameter(value = 1) + public String propPath; + + @Parameterized.Parameter(value = 2) + public boolean safe; + + @Parameterized.Parameter(value = 3) + public XstsConfigBuilder.Domain domain; + + @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}, {3}") + public static Collection data() { + return Arrays.asList(new Object[][] { + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival1.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival1.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival2.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival2.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival3.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival3.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival4.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival4.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival5.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival5.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival6.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival6.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival7.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival7.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival8.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival8.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival9.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival9.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival10.prop", false, XstsConfigBuilder.Domain.EXPL}, + + { "src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts", "src/test/resources/property/antival10.prop", false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + + }); + } + + @Test + public void test() throws IOException { + + final Logger logger = new ConsoleLogger(Level.SUBSTEP); + + 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) + .optimizeStmts(XstsConfigBuilder.OptimizeStmts.ON) + .predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS) + .maxEnum(250) + .autoExpl(XstsConfigBuilder.AutoExpl.NEWOPERANDS) + .clockImpl(XstsConfigBuilder.ClockImpl.RAT) + .pruneStrategy(PruneStrategy.FULL) + .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/ANTIVAL_CHK_COID_System.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/ANTIVAL_CHK_COID_System.xsts new file mode 100644 index 0000000000..d75ec08bb3 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/ANTIVAL_CHK_COID_System.xsts @@ -0,0 +1,681 @@ +type MyBool : { ERVENYTELEN, _0, _1 } +type Main_region_of_mo_antivalchk_AntivalenceChecker : { __Inactive__, _1_0, Hibatarolassal_0_1, Hibatarolassal_1_2, Hibatarolassal_0_rol_1_re_3, _1_rol_0_ra_4, _0_5, _0_rol_1_re_6, Hibatarolassal_1_rol_0_ra_7, Hibaallapot_8 } +type Activeness : { ACTIVE, PASSIVE } +type CeloldasIdozites : { CELOLDAS_IDOZITES, NINCS_CELOLDAS_IDOZITES, NERV1 } +type Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep : { __Inactive__, Oldas_4, Celoldas_idozites_nem_fut_5, Celoldas_idozites_fut_8 } +type Region_1_in_Celoldas_idozites_nem_fut_5_bJbCOID_allapotgep : { __Inactive__, Ervenytelen_0, Tranziens_2, Idozites_nem_fut_1 } +var Signals_p_In_antival_chk_I_CR : boolean = false +var Signals_p_In_pValue_antival_chk_I_CR : MyBool = ERVENYTELEN +var Signals_n_In_antival_chk_I_CR : boolean = false +var Signals_n_In_nValue_antival_chk_I_CR : MyBool = ERVENYTELEN +ctrl var main_region_of_mo_antivalchk_antival_chk_I_CR : Main_region_of_mo_antivalchk_AntivalenceChecker = __Inactive__ +ctrl var _0_rol_1_re_6Timeout_antival_chk_I_CR : integer = 0 +var Signals_p_In_antival_chk_I_FT : boolean = false +var Signals_p_In_pValue_antival_chk_I_FT : MyBool = ERVENYTELEN +var Signals_n_In_antival_chk_I_FT : boolean = false +var Signals_n_In_nValue_antival_chk_I_FT : MyBool = ERVENYTELEN +ctrl var main_region_of_mo_antivalchk_antival_chk_I_FT : Main_region_of_mo_antivalchk_AntivalenceChecker = __Inactive__ +ctrl var _0_rol_1_re_6Timeout_antival_chk_I_FT : integer = 0 +var I_FT_h_In_coid : boolean = false +var I_FT_h_In_hValue_coid : MyBool = ERVENYTELEN +var StateMachine_OutPort_O_COID_Out_coid : boolean = false +var StateMachine_OutPort_O_COID_Out_O_COIDValue_coid : Activeness = ACTIVE +var I_CR_h_In_coid : boolean = false +var I_CR_h_In_hValue_coid : MyBool = ERVENYTELEN +var I_FT_e_In_coid : boolean = false +var I_FT_e_In_eValue_coid : MyBool = ERVENYTELEN +ctrl var main_region_of_bJbCOID_allapotgep_coid : Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep = __Inactive__ +ctrl var region_1_in_Celoldas_idozites_nem_fut_5_coid : Region_1_in_Celoldas_idozites_nem_fut_5_bJbCOID_allapotgep = __Inactive__ + var __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid : boolean = false + var __id_Celoldas_idozites_fut_8_1_Oldas_4__coid : boolean = false + var __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid : boolean = false + var __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid : boolean = false +var Oldas_Exit_coid : boolean = false + var __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid : boolean = false + var __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid : boolean = false + var __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid : boolean = false + var __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid : boolean = false + var Fut_NemFut_coid : boolean = false + var __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid : boolean = false +var RS_COID_coid : CeloldasIdozites = CELOLDAS_IDOZITES +ctrl var P_COIDT_Timeout_coid : integer = 0 +ctrl var P_COIDH_Timeout_coid : integer = 0 + +trans { + _0_rol_1_re_6Timeout_antival_chk_I_CR := (if (_0_rol_1_re_6Timeout_antival_chk_I_CR < 503) then (_0_rol_1_re_6Timeout_antival_chk_I_CR + 495) else _0_rol_1_re_6Timeout_antival_chk_I_CR); + _0_rol_1_re_6Timeout_antival_chk_I_FT := (if (_0_rol_1_re_6Timeout_antival_chk_I_FT < 501) then (_0_rol_1_re_6Timeout_antival_chk_I_FT + 495) else _0_rol_1_re_6Timeout_antival_chk_I_FT); + P_COIDT_Timeout_coid := (if (P_COIDT_Timeout_coid < 497) then (P_COIDT_Timeout_coid + 495) else P_COIDT_Timeout_coid); + P_COIDH_Timeout_coid := (if (P_COIDH_Timeout_coid < 499) then (P_COIDH_Timeout_coid + 495) else P_COIDH_Timeout_coid); + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_0_rol_1_re_3) && (503 <= _0_rol_1_re_6Timeout_antival_chk_I_CR))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == _1_rol_0_ra_4) && (503 <= _0_rol_1_re_6Timeout_antival_chk_I_CR))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == _0_rol_1_re_6) && (503 <= _0_rol_1_re_6Timeout_antival_chk_I_CR))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_1_rol_0_ra_7) && (503 <= _0_rol_1_re_6Timeout_antival_chk_I_CR))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_CR == _1_0)) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if ((((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _1)) || (Signals_p_In_pValue_antival_chk_I_CR == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_CR == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_rol_0_ra_4; + _0_rol_1_re_6Timeout_antival_chk_I_CR := 0; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_0_1)) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + else { + if ((((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _1)) || (Signals_p_In_pValue_antival_chk_I_CR == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_CR == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_0_rol_1_re_3; + _0_rol_1_re_6Timeout_antival_chk_I_CR := 0; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_0_1; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_CR == _0_5)) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if ((((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _1)) || (Signals_p_In_pValue_antival_chk_I_CR == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_CR == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_rol_1_re_6; + _0_rol_1_re_6Timeout_antival_chk_I_CR := 0; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_1_rol_0_ra_7) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_1_2; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == _0_rol_1_re_6) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_1_2)) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + if ((((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _1)) || (Signals_p_In_pValue_antival_chk_I_CR == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_CR == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_1_rol_0_ra_7; + _0_rol_1_re_6Timeout_antival_chk_I_CR := 0; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_1_2; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibaallapot_8) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1) && (true == true))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_0_1; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0) && (true == true))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_1_2; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_0_rol_1_re_3) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_0_1; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == _1_rol_0_ra_4) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_0_rol_1_re_3) && (501 <= _0_rol_1_re_6Timeout_antival_chk_I_FT))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == _1_rol_0_ra_4) && (501 <= _0_rol_1_re_6Timeout_antival_chk_I_FT))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == _0_rol_1_re_6) && (501 <= _0_rol_1_re_6Timeout_antival_chk_I_FT))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_1_rol_0_ra_7) && (501 <= _0_rol_1_re_6Timeout_antival_chk_I_FT))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_FT == _1_0)) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if ((((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _1)) || (Signals_p_In_pValue_antival_chk_I_FT == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_FT == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_rol_0_ra_4; + _0_rol_1_re_6Timeout_antival_chk_I_FT := 0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_0_1)) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + else { + if ((((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _1)) || (Signals_p_In_pValue_antival_chk_I_FT == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_FT == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_0_rol_1_re_3; + _0_rol_1_re_6Timeout_antival_chk_I_FT := 0; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_0_1; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_FT == _0_5)) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if ((((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _1)) || (Signals_p_In_pValue_antival_chk_I_FT == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_FT == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_rol_1_re_6; + _0_rol_1_re_6Timeout_antival_chk_I_FT := 0; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_1_rol_0_ra_7) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_1_2; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == _0_rol_1_re_6) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_1_2)) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + if ((((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _1)) || (Signals_p_In_pValue_antival_chk_I_FT == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_FT == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_1_rol_0_ra_7; + _0_rol_1_re_6Timeout_antival_chk_I_FT := 0; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_1_2; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibaallapot_8) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1) && (true == true))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_0_1; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0) && (true == true))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_1_2; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_0_rol_1_re_3) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_0_1; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == _1_rol_0_ra_4) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid := false; + __id_Celoldas_idozites_fut_8_1_Oldas_4__coid := false; + __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid := false; + __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid := false; + __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid := false; + __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid := false; + Fut_NemFut_coid := false; + __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid := false; + if (((region_1_in_Celoldas_idozites_nem_fut_5_coid == Ervenytelen_0) && (I_FT_e_In_eValue_coid == _0))) { + __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid := true; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Idozites_nem_fut_1; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; + } + else { + if (((region_1_in_Celoldas_idozites_nem_fut_5_coid == Idozites_nem_fut_1) && (I_FT_h_In_hValue_coid != _0))) { + __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid := true; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Ervenytelen_0; + RS_COID_coid := NERV1; + } + else { + if (((region_1_in_Celoldas_idozites_nem_fut_5_coid == Tranziens_2) && (497 <= P_COIDT_Timeout_coid))) { + region_1_in_Celoldas_idozites_nem_fut_5_coid := __Inactive__; + __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid := true; + choice { + assume (I_FT_e_In_eValue_coid == _0); + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid := true; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Idozites_nem_fut_1; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; + } or { + assume (I_FT_e_In_eValue_coid != _0); + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid := true; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Ervenytelen_0; + RS_COID_coid := NERV1; + } or { + assume (!(((I_FT_e_In_eValue_coid == _0) || (I_FT_e_In_eValue_coid != _0)))); + } + } + else { + choice { + assume ((main_region_of_bJbCOID_allapotgep_coid == Oldas_4) && ((I_CR_h_In_hValue_coid != _1) || (I_FT_h_In_hValue_coid != _1))); + Oldas_Exit_coid := true; + __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid := true; + main_region_of_bJbCOID_allapotgep_coid := Celoldas_idozites_nem_fut_5; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Tranziens_2; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := PASSIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + P_COIDT_Timeout_coid := 0; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; + } or { + assume ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_nem_fut_5) && (I_CR_h_In_hValue_coid == _1) && (I_FT_h_In_hValue_coid == _1)); + region_1_in_Celoldas_idozites_nem_fut_5_coid := __Inactive__; + __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid := true; + main_region_of_bJbCOID_allapotgep_coid := Celoldas_idozites_fut_8; + P_COIDH_Timeout_coid := 0; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := PASSIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + RS_COID_coid := CELOLDAS_IDOZITES; + } or { + assume ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_fut_8) && (499 <= P_COIDH_Timeout_coid) && (I_CR_h_In_hValue_coid == _1) && (I_FT_h_In_hValue_coid == _1)); + __id_Celoldas_idozites_fut_8_1_Oldas_4__coid := true; + main_region_of_bJbCOID_allapotgep_coid := Oldas_4; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := ACTIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + RS_COID_coid := CELOLDAS_IDOZITES; + } or { + assume ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_fut_8) && ((I_CR_h_In_hValue_coid != _1) || (I_FT_h_In_hValue_coid != _1))); + Fut_NemFut_coid := true; + main_region_of_bJbCOID_allapotgep_coid := Celoldas_idozites_nem_fut_5; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Tranziens_2; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := PASSIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + P_COIDT_Timeout_coid := 0; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; + } or { + assume (!((((main_region_of_bJbCOID_allapotgep_coid == Oldas_4) && ((I_CR_h_In_hValue_coid != _1) || (I_FT_h_In_hValue_coid != _1))) || ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_nem_fut_5) && (I_CR_h_In_hValue_coid == _1) && (I_FT_h_In_hValue_coid == _1)) || ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_fut_8) && (499 <= P_COIDH_Timeout_coid) && (I_CR_h_In_hValue_coid == _1) && (I_FT_h_In_hValue_coid == _1)) || ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_fut_8) && ((I_CR_h_In_hValue_coid != _1) || (I_FT_h_In_hValue_coid != _1)))))); + } + } + } + } + I_FT_h_In_coid := false; + I_FT_e_In_coid := false; + I_CR_h_In_coid := false; + Signals_p_In_antival_chk_I_FT := false; + Signals_n_In_antival_chk_I_CR := false; + Signals_p_In_antival_chk_I_CR := false; + Signals_n_In_antival_chk_I_FT := false; +} +init { + _0_rol_1_re_6Timeout_antival_chk_I_CR := (503 + 503 + 503 + 503); + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + Signals_p_In_antival_chk_I_CR := false; + Signals_n_In_antival_chk_I_CR := false; + Signals_p_In_pValue_antival_chk_I_CR := ERVENYTELEN; + Signals_n_In_nValue_antival_chk_I_CR := ERVENYTELEN; + _0_rol_1_re_6Timeout_antival_chk_I_FT := (501 + 501 + 501 + 501); + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + Signals_p_In_antival_chk_I_FT := false; + Signals_n_In_antival_chk_I_FT := false; + Signals_p_In_pValue_antival_chk_I_FT := ERVENYTELEN; + Signals_n_In_nValue_antival_chk_I_FT := ERVENYTELEN; + RS_COID_coid := CELOLDAS_IDOZITES; + Oldas_Exit_coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid := false; + __id_Celoldas_idozites_fut_8_1_Oldas_4__coid := false; + __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid := false; + __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid := false; + __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid := false; + __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid := false; + Fut_NemFut_coid := false; + __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid := false; + __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid := false; + P_COIDH_Timeout_coid := 499; + P_COIDT_Timeout_coid := 497; + main_region_of_bJbCOID_allapotgep_coid := __Inactive__; + region_1_in_Celoldas_idozites_nem_fut_5_coid := __Inactive__; + I_FT_h_In_coid := false; + I_CR_h_In_coid := false; + I_FT_e_In_coid := false; + StateMachine_OutPort_O_COID_Out_coid := false; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_FT_e_In_eValue_coid := ERVENYTELEN; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := ACTIVE; + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid := true; + main_region_of_bJbCOID_allapotgep_coid := Celoldas_idozites_nem_fut_5; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Tranziens_2; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := PASSIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + P_COIDT_Timeout_coid := 0; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; +} +env { + __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid := false; + __id_Celoldas_idozites_fut_8_1_Oldas_4__coid := false; + __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid := false; + __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid := false; + __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid := false; + __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid := false; + Fut_NemFut_coid := false; + __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid := false; + havoc Signals_p_In_antival_chk_I_CR; + if (Signals_p_In_antival_chk_I_CR) { + havoc Signals_p_In_pValue_antival_chk_I_CR; + } + havoc Signals_n_In_antival_chk_I_CR; + if (Signals_n_In_antival_chk_I_CR) { + havoc Signals_n_In_nValue_antival_chk_I_CR; + } + havoc Signals_p_In_antival_chk_I_FT; + if (Signals_p_In_antival_chk_I_FT) { + havoc Signals_p_In_pValue_antival_chk_I_FT; + } + havoc Signals_n_In_antival_chk_I_FT; + if (Signals_n_In_antival_chk_I_FT) { + havoc Signals_n_In_nValue_antival_chk_I_FT; + } + Signals_p_In_antival_chk_I_FT := Signals_p_In_antival_chk_I_CR; + Signals_n_In_antival_chk_I_FT := Signals_n_In_antival_chk_I_CR; + Signals_p_In_pValue_antival_chk_I_FT := Signals_p_In_pValue_antival_chk_I_CR; + Signals_n_In_nValue_antival_chk_I_FT := Signals_n_In_nValue_antival_chk_I_CR; + StateMachine_OutPort_O_COID_Out_coid := false; +} diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts new file mode 100644 index 0000000000..37a1c305d6 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/ANTIVAL_CHK_COID_System_timed.xsts @@ -0,0 +1,678 @@ +type MyBool : { ERVENYTELEN, _0, _1 } +type Main_region_of_mo_antivalchk_AntivalenceChecker : { __Inactive__, _1_0, Hibatarolassal_0_1, Hibatarolassal_1_2, Hibatarolassal_0_rol_1_re_3, _1_rol_0_ra_4, _0_5, _0_rol_1_re_6, Hibatarolassal_1_rol_0_ra_7, Hibaallapot_8 } +type Activeness : { ACTIVE, PASSIVE } +type CeloldasIdozites : { CELOLDAS_IDOZITES, NINCS_CELOLDAS_IDOZITES, NERV1 } +type Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep : { __Inactive__, Oldas_4, Celoldas_idozites_nem_fut_5, Celoldas_idozites_fut_8 } +type Region_1_in_Celoldas_idozites_nem_fut_5_bJbCOID_allapotgep : { __Inactive__, Ervenytelen_0, Tranziens_2, Idozites_nem_fut_1 } +var Signals_p_In_antival_chk_I_CR : boolean = false +var Signals_p_In_pValue_antival_chk_I_CR : MyBool = ERVENYTELEN +var Signals_n_In_antival_chk_I_CR : boolean = false +var Signals_n_In_nValue_antival_chk_I_CR : MyBool = ERVENYTELEN +ctrl var main_region_of_mo_antivalchk_antival_chk_I_CR : Main_region_of_mo_antivalchk_AntivalenceChecker = __Inactive__ +var _0_rol_1_re_6Timeout_antival_chk_I_CR : clock +var Signals_p_In_antival_chk_I_FT : boolean = false +var Signals_p_In_pValue_antival_chk_I_FT : MyBool = ERVENYTELEN +var Signals_n_In_antival_chk_I_FT : boolean = false +var Signals_n_In_nValue_antival_chk_I_FT : MyBool = ERVENYTELEN +ctrl var main_region_of_mo_antivalchk_antival_chk_I_FT : Main_region_of_mo_antivalchk_AntivalenceChecker = __Inactive__ +var _0_rol_1_re_6Timeout_antival_chk_I_FT : clock +var I_FT_h_In_coid : boolean = false +var I_FT_h_In_hValue_coid : MyBool = ERVENYTELEN +var StateMachine_OutPort_O_COID_Out_coid : boolean = false +var StateMachine_OutPort_O_COID_Out_O_COIDValue_coid : Activeness = ACTIVE +var I_CR_h_In_coid : boolean = false +var I_CR_h_In_hValue_coid : MyBool = ERVENYTELEN +var I_FT_e_In_coid : boolean = false +var I_FT_e_In_eValue_coid : MyBool = ERVENYTELEN +ctrl var main_region_of_bJbCOID_allapotgep_coid : Main_region_of_bJbCOID_allapotgep_bJbCOID_allapotgep = __Inactive__ +ctrl var region_1_in_Celoldas_idozites_nem_fut_5_coid : Region_1_in_Celoldas_idozites_nem_fut_5_bJbCOID_allapotgep = __Inactive__ + var __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid : boolean = false + var __id_Celoldas_idozites_fut_8_1_Oldas_4__coid : boolean = false + var __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid : boolean = false + var __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid : boolean = false +var Oldas_Exit_coid : boolean = false + var __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid : boolean = false + var __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid : boolean = false + var __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid : boolean = false + var __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid : boolean = false + var Fut_NemFut_coid : boolean = false + var __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid : boolean = false +var RS_COID_coid : CeloldasIdozites = CELOLDAS_IDOZITES +var P_COIDT_Timeout_coid : clock +var P_COIDH_Timeout_coid : clock + +trans { + __delay; + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_0_rol_1_re_3) && (503 <= _0_rol_1_re_6Timeout_antival_chk_I_CR))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == _1_rol_0_ra_4) && (503 <= _0_rol_1_re_6Timeout_antival_chk_I_CR))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == _0_rol_1_re_6) && (503 <= _0_rol_1_re_6Timeout_antival_chk_I_CR))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_1_rol_0_ra_7) && (503 <= _0_rol_1_re_6Timeout_antival_chk_I_CR))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_CR == _1_0)) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if ((((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _1)) || (Signals_p_In_pValue_antival_chk_I_CR == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_CR == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_rol_0_ra_4; + _0_rol_1_re_6Timeout_antival_chk_I_CR := 0; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_0_1)) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + else { + if ((((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _1)) || (Signals_p_In_pValue_antival_chk_I_CR == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_CR == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_0_rol_1_re_3; + _0_rol_1_re_6Timeout_antival_chk_I_CR := 0; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_0_1; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_CR == _0_5)) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if ((((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _1)) || (Signals_p_In_pValue_antival_chk_I_CR == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_CR == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_rol_1_re_6; + _0_rol_1_re_6Timeout_antival_chk_I_CR := 0; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_1_rol_0_ra_7) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_1_2; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == _0_rol_1_re_6) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_1_2)) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + if ((((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _1)) || (Signals_p_In_pValue_antival_chk_I_CR == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_CR == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_1_rol_0_ra_7; + _0_rol_1_re_6Timeout_antival_chk_I_CR := 0; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_1_2; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibaallapot_8) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1) && (true == true))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_0_1; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0) && (true == true))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_1_2; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_0_rol_1_re_3) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibatarolassal_0_1; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_CR == _1_rol_0_ra_4) && (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0)) || ((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_CR == _0) && (Signals_n_In_nValue_antival_chk_I_CR == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _0_5; + I_CR_h_In_hValue_coid := _0; + I_CR_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_CR == _1) && (Signals_n_In_nValue_antival_chk_I_CR == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_CR := _1_0; + I_CR_h_In_hValue_coid := _1; + I_CR_h_In_coid := true; + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_0_rol_1_re_3) && (501 <= _0_rol_1_re_6Timeout_antival_chk_I_FT))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == _1_rol_0_ra_4) && (501 <= _0_rol_1_re_6Timeout_antival_chk_I_FT))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == _0_rol_1_re_6) && (501 <= _0_rol_1_re_6Timeout_antival_chk_I_FT))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_1_rol_0_ra_7) && (501 <= _0_rol_1_re_6Timeout_antival_chk_I_FT))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_FT == _1_0)) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if ((((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _1)) || (Signals_p_In_pValue_antival_chk_I_FT == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_FT == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_rol_0_ra_4; + _0_rol_1_re_6Timeout_antival_chk_I_FT := 0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_0_1)) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + else { + if ((((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _1)) || (Signals_p_In_pValue_antival_chk_I_FT == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_FT == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_0_rol_1_re_3; + _0_rol_1_re_6Timeout_antival_chk_I_FT := 0; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_0_1; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_FT == _0_5)) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if ((((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _1)) || (Signals_p_In_pValue_antival_chk_I_FT == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_FT == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_rol_1_re_6; + _0_rol_1_re_6Timeout_antival_chk_I_FT := 0; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_1_rol_0_ra_7) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_1_2; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == _0_rol_1_re_6) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + } + } + else { + if ((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_1_2)) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + if ((((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _1)) || (Signals_p_In_pValue_antival_chk_I_FT == ERVENYTELEN) || (Signals_n_In_nValue_antival_chk_I_FT == ERVENYTELEN))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_1_rol_0_ra_7; + _0_rol_1_re_6Timeout_antival_chk_I_FT := 0; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_1_2; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibaallapot_8) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1) && (true == true))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_0_1; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0) && (true == true))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_1_2; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_0_rol_1_re_3) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibatarolassal_0_1; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + } + } + } + else { + if (((main_region_of_mo_antivalchk_antival_chk_I_FT == _1_rol_0_ra_4) && (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0)) || ((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + if (((Signals_p_In_pValue_antival_chk_I_FT == _0) && (Signals_n_In_nValue_antival_chk_I_FT == _1))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _0_5; + I_FT_e_In_eValue_coid := _0; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _0; + I_FT_h_In_coid := true; + } + else { + if (((Signals_p_In_pValue_antival_chk_I_FT == _1) && (Signals_n_In_nValue_antival_chk_I_FT == _0))) { + main_region_of_mo_antivalchk_antival_chk_I_FT := _1_0; + I_FT_e_In_eValue_coid := _1; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := _1; + I_FT_h_In_coid := true; + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid := false; + __id_Celoldas_idozites_fut_8_1_Oldas_4__coid := false; + __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid := false; + __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid := false; + __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid := false; + __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid := false; + Fut_NemFut_coid := false; + __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid := false; + if (((region_1_in_Celoldas_idozites_nem_fut_5_coid == Ervenytelen_0) && (I_FT_e_In_eValue_coid == _0))) { + __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid := true; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Idozites_nem_fut_1; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; + } + else { + if (((region_1_in_Celoldas_idozites_nem_fut_5_coid == Idozites_nem_fut_1) && (I_FT_h_In_hValue_coid != _0))) { + __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid := true; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Ervenytelen_0; + RS_COID_coid := NERV1; + } + else { + if (((region_1_in_Celoldas_idozites_nem_fut_5_coid == Tranziens_2) && (497 <= P_COIDT_Timeout_coid))) { + region_1_in_Celoldas_idozites_nem_fut_5_coid := __Inactive__; + __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid := true; + choice { + assume (I_FT_e_In_eValue_coid == _0); + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid := true; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Idozites_nem_fut_1; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; + } or { + assume (I_FT_e_In_eValue_coid != _0); + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid := true; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Ervenytelen_0; + RS_COID_coid := NERV1; + } or { + assume (!(((I_FT_e_In_eValue_coid == _0) || (I_FT_e_In_eValue_coid != _0)))); + } + } + else { + choice { + assume ((main_region_of_bJbCOID_allapotgep_coid == Oldas_4) && ((I_CR_h_In_hValue_coid != _1) || (I_FT_h_In_hValue_coid != _1))); + Oldas_Exit_coid := true; + __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid := true; + main_region_of_bJbCOID_allapotgep_coid := Celoldas_idozites_nem_fut_5; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Tranziens_2; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := PASSIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + P_COIDT_Timeout_coid := 0; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; + } or { + assume ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_nem_fut_5) && (I_CR_h_In_hValue_coid == _1) && (I_FT_h_In_hValue_coid == _1)); + region_1_in_Celoldas_idozites_nem_fut_5_coid := __Inactive__; + __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid := true; + main_region_of_bJbCOID_allapotgep_coid := Celoldas_idozites_fut_8; + P_COIDH_Timeout_coid := 0; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := PASSIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + RS_COID_coid := CELOLDAS_IDOZITES; + } or { + assume ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_fut_8) && (499 <= P_COIDH_Timeout_coid) && (I_CR_h_In_hValue_coid == _1) && (I_FT_h_In_hValue_coid == _1)); + __id_Celoldas_idozites_fut_8_1_Oldas_4__coid := true; + main_region_of_bJbCOID_allapotgep_coid := Oldas_4; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := ACTIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + RS_COID_coid := CELOLDAS_IDOZITES; + } or { + assume ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_fut_8) && ((I_CR_h_In_hValue_coid != _1) || (I_FT_h_In_hValue_coid != _1))); + Fut_NemFut_coid := true; + main_region_of_bJbCOID_allapotgep_coid := Celoldas_idozites_nem_fut_5; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Tranziens_2; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := PASSIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + P_COIDT_Timeout_coid := 0; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; + } or { + assume (!((((main_region_of_bJbCOID_allapotgep_coid == Oldas_4) && ((I_CR_h_In_hValue_coid != _1) || (I_FT_h_In_hValue_coid != _1))) || ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_nem_fut_5) && (I_CR_h_In_hValue_coid == _1) && (I_FT_h_In_hValue_coid == _1)) || ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_fut_8) && (499 <= P_COIDH_Timeout_coid) && (I_CR_h_In_hValue_coid == _1) && (I_FT_h_In_hValue_coid == _1)) || ((main_region_of_bJbCOID_allapotgep_coid == Celoldas_idozites_fut_8) && ((I_CR_h_In_hValue_coid != _1) || (I_FT_h_In_hValue_coid != _1)))))); + } + } + } + } + I_FT_h_In_coid := false; + I_FT_e_In_coid := false; + I_CR_h_In_coid := false; + Signals_p_In_antival_chk_I_FT := false; + Signals_n_In_antival_chk_I_CR := false; + Signals_p_In_antival_chk_I_CR := false; + Signals_n_In_antival_chk_I_FT := false; +} +init { + _0_rol_1_re_6Timeout_antival_chk_I_CR := (503 + 503 + 503 + 503); + main_region_of_mo_antivalchk_antival_chk_I_CR := __Inactive__; + Signals_p_In_antival_chk_I_CR := false; + Signals_n_In_antival_chk_I_CR := false; + Signals_p_In_pValue_antival_chk_I_CR := ERVENYTELEN; + Signals_n_In_nValue_antival_chk_I_CR := ERVENYTELEN; + _0_rol_1_re_6Timeout_antival_chk_I_FT := (501 + 501 + 501 + 501); + main_region_of_mo_antivalchk_antival_chk_I_FT := __Inactive__; + Signals_p_In_antival_chk_I_FT := false; + Signals_n_In_antival_chk_I_FT := false; + Signals_p_In_pValue_antival_chk_I_FT := ERVENYTELEN; + Signals_n_In_nValue_antival_chk_I_FT := ERVENYTELEN; + RS_COID_coid := CELOLDAS_IDOZITES; + Oldas_Exit_coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid := false; + __id_Celoldas_idozites_fut_8_1_Oldas_4__coid := false; + __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid := false; + __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid := false; + __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid := false; + __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid := false; + Fut_NemFut_coid := false; + __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid := false; + __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid := false; + P_COIDH_Timeout_coid := 499; + P_COIDT_Timeout_coid := 497; + main_region_of_bJbCOID_allapotgep_coid := __Inactive__; + region_1_in_Celoldas_idozites_nem_fut_5_coid := __Inactive__; + I_FT_h_In_coid := false; + I_CR_h_In_coid := false; + I_FT_e_In_coid := false; + StateMachine_OutPort_O_COID_Out_coid := false; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_FT_e_In_eValue_coid := ERVENYTELEN; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := ACTIVE; + main_region_of_mo_antivalchk_antival_chk_I_CR := Hibaallapot_8; + main_region_of_mo_antivalchk_antival_chk_I_FT := Hibaallapot_8; + __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid := true; + main_region_of_bJbCOID_allapotgep_coid := Celoldas_idozites_nem_fut_5; + region_1_in_Celoldas_idozites_nem_fut_5_coid := Tranziens_2; + I_CR_h_In_hValue_coid := ERVENYTELEN; + I_CR_h_In_coid := true; + I_FT_e_In_eValue_coid := ERVENYTELEN; + I_FT_e_In_coid := true; + I_FT_h_In_hValue_coid := ERVENYTELEN; + I_FT_h_In_coid := true; + StateMachine_OutPort_O_COID_Out_O_COIDValue_coid := PASSIVE; + StateMachine_OutPort_O_COID_Out_coid := true; + P_COIDT_Timeout_coid := 0; + RS_COID_coid := NINCS_CELOLDAS_IDOZITES; +} +env { + __id_Idozites_nem_fut_1_8_Ervenytelen_0__coid := false; + __id_Celoldas_idozites_fut_8_1_Oldas_4__coid := false; + __id_Ervenytelen_0_2_Idozites_nem_fut_1__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid := false; + __id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid := false; + __id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid := false; + __id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid := false; + __id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid := false; + Fut_NemFut_coid := false; + __id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid := false; + havoc Signals_p_In_antival_chk_I_CR; + if (Signals_p_In_antival_chk_I_CR) { + havoc Signals_p_In_pValue_antival_chk_I_CR; + } + havoc Signals_n_In_antival_chk_I_CR; + if (Signals_n_In_antival_chk_I_CR) { + havoc Signals_n_In_nValue_antival_chk_I_CR; + } + havoc Signals_p_In_antival_chk_I_FT; + if (Signals_p_In_antival_chk_I_FT) { + havoc Signals_p_In_pValue_antival_chk_I_FT; + } + havoc Signals_n_In_antival_chk_I_FT; + if (Signals_n_In_antival_chk_I_FT) { + havoc Signals_n_In_nValue_antival_chk_I_FT; + } + Signals_p_In_antival_chk_I_FT := Signals_p_In_antival_chk_I_CR; + Signals_n_In_antival_chk_I_FT := Signals_n_In_antival_chk_I_CR; + Signals_p_In_pValue_antival_chk_I_FT := Signals_p_In_pValue_antival_chk_I_CR; + Signals_n_In_nValue_antival_chk_I_FT := Signals_n_In_nValue_antival_chk_I_CR; + StateMachine_OutPort_O_COID_Out_coid := false; +} diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/Crossroad-Theta.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/Crossroad-Theta.xsts new file mode 100644 index 0000000000..cc3c8c8ea0 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/Crossroad-Theta.xsts @@ -0,0 +1,326 @@ +type Main_region_Controller : { __Inactive__, Operating } +type Operating_Controller : { __Inactive__, Init, PriorityPrepares, Priority, Secondary, SecondaryPrepares, Init_Inactive_, PriorityPrepares_Inactive_, Priority_Inactive_, Secondary_Inactive_, SecondaryPrepares_Inactive_ } +type Main_region_TrafficLightCtrl : { __Inactive__, Interrupted, Normal } +type Interrupted_TrafficLightCtrl : { __Inactive__, Black, BlinkingYellow } +type Normal_TrafficLightCtrl : { __Inactive__, Red, Yellow, Green, Red_Inactive_, Yellow_Inactive_, Green_Inactive_ } +var PoliceInterrupt_police_In_controller : boolean = false +ctrl var main_region_controller : Main_region_Controller = __Inactive__ +ctrl var operating_controller : Operating_Controller = __Inactive__ +ctrl var InitTimeout3_controller : integer = 0 +var PoliceInterrupt_police_In_prior : boolean = false +var LightCommands_displayNone_Out_prior : boolean = false +var Control_toggle_In_prior : boolean = false +var LightCommands_displayRed_Out_prior : boolean = false +var LightCommands_displayGreen_Out_prior : boolean = false +var LightCommands_displayYellow_Out_prior : boolean = false +ctrl var main_region_prior : Main_region_TrafficLightCtrl = __Inactive__ +ctrl var interrupted_prior : Interrupted_TrafficLightCtrl = __Inactive__ +ctrl var normal_prior : Normal_TrafficLightCtrl = __Inactive__ +var asd_prior : integer = 0 +var b_prior : integer = 0 +var a_prior : boolean = false +ctrl var BlinkingYellowTimeout3_prior : integer = 0 +var LightCommands_displayGreen_Out_second : boolean = false +var PoliceInterrupt_police_In_second : boolean = false +var LightCommands_displayNone_Out_second : boolean = false +var LightCommands_displayRed_Out_second : boolean = false +var LightCommands_displayYellow_Out_second : boolean = false +var Control_toggle_In_second : boolean = false +ctrl var main_region_second : Main_region_TrafficLightCtrl = __Inactive__ +ctrl var normal_second : Normal_TrafficLightCtrl = __Inactive__ +ctrl var interrupted_second : Interrupted_TrafficLightCtrl = __Inactive__ +var asd_second : integer = 0 +var a_second : boolean = false +var b_second : integer = 0 +ctrl var BlinkingYellowTimeout3_second : integer = 0 + +trans { + InitTimeout3_controller := (if (InitTimeout3_controller < 2000) then (InitTimeout3_controller + 500) else InitTimeout3_controller); + BlinkingYellowTimeout3_prior := (if (BlinkingYellowTimeout3_prior < 500) then (BlinkingYellowTimeout3_prior + 500) else BlinkingYellowTimeout3_prior); + BlinkingYellowTimeout3_second := (if (BlinkingYellowTimeout3_second < 500) then (BlinkingYellowTimeout3_second + 500) else BlinkingYellowTimeout3_second); + if (((main_region_controller == Operating) && PoliceInterrupt_police_In_controller)) { + operating_controller := (if (operating_controller == Init) then Init_Inactive_ else (if (operating_controller == PriorityPrepares) then PriorityPrepares_Inactive_ else (if (operating_controller == Priority) then Priority_Inactive_ else (if (operating_controller == Secondary) then Secondary_Inactive_ else SecondaryPrepares_Inactive_)))); + PoliceInterrupt_police_In_prior := true; + PoliceInterrupt_police_In_second := true; + main_region_controller := Operating; + if ((operating_controller == __Inactive__)) { + operating_controller := Init; + } + else { + operating_controller := (if (operating_controller == Init_Inactive_) then Init else (if (operating_controller == PriorityPrepares_Inactive_) then PriorityPrepares else (if (operating_controller == Priority_Inactive_) then Priority else (if (operating_controller == Secondary_Inactive_) then Secondary else SecondaryPrepares)))); + } + if ((operating_controller == Init)) { + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + } + else { + if ((operating_controller == PriorityPrepares)) { + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + } + else { + if ((operating_controller == Priority)) { + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + Control_toggle_In_second := true; + } + else { + if ((operating_controller == Secondary)) { + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + Control_toggle_In_second := true; + } + else { + if ((operating_controller == SecondaryPrepares)) { + InitTimeout3_controller := 0; + Control_toggle_In_second := true; + } + } + } + } + } + } + else { + if (((operating_controller == Init) && ((2 * 1000) <= InitTimeout3_controller))) { + operating_controller := PriorityPrepares; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + } + else { + if (((operating_controller == PriorityPrepares) && ((1 * 1000) <= InitTimeout3_controller))) { + operating_controller := Secondary; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + Control_toggle_In_second := true; + } + else { + if (((operating_controller == Priority) && ((2 * 1000) <= InitTimeout3_controller) && (true != false))) { + operating_controller := PriorityPrepares; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + } + else { + if (((operating_controller == Secondary) && ((2 * 1000) <= InitTimeout3_controller))) { + operating_controller := SecondaryPrepares; + InitTimeout3_controller := 0; + Control_toggle_In_second := true; + } + else { + if (((operating_controller == SecondaryPrepares) && ((1 * 1000) <= InitTimeout3_controller))) { + operating_controller := Priority; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + Control_toggle_In_second := true; + } + } + } + } + } + } + if (((main_region_prior == Interrupted) && PoliceInterrupt_police_In_prior)) { + interrupted_prior := __Inactive__; + main_region_prior := Normal; + if ((normal_prior == __Inactive__)) { + normal_prior := Red; + } + else { + normal_prior := (if (normal_prior == Red_Inactive_) then Red else (if (normal_prior == Yellow_Inactive_) then Yellow else Green)); + } + if ((normal_prior == Red)) { + LightCommands_displayRed_Out_prior := true; + } + else { + if ((normal_prior == Yellow)) { + LightCommands_displayYellow_Out_prior := true; + } + else { + if ((normal_prior == Green)) { + LightCommands_displayGreen_Out_prior := true; + } + } + } + } + else { + if (((main_region_prior == Normal) && PoliceInterrupt_police_In_prior)) { + if ((main_region_prior == Normal)) { + if ((normal_prior == Red)) { + a_prior := true; + } + asd_prior := 321; + } + normal_prior := (if (normal_prior == Red) then Red_Inactive_ else (if (normal_prior == Yellow) then Yellow_Inactive_ else Green_Inactive_)); + main_region_prior := Interrupted; + interrupted_prior := BlinkingYellow; + BlinkingYellowTimeout3_prior := 0; + LightCommands_displayYellow_Out_prior := true; + } + else { + if (((interrupted_prior == Black) && (500 <= BlinkingYellowTimeout3_prior))) { + interrupted_prior := BlinkingYellow; + BlinkingYellowTimeout3_prior := 0; + LightCommands_displayYellow_Out_prior := true; + } + else { + if (((interrupted_prior == BlinkingYellow) && (500 <= BlinkingYellowTimeout3_prior))) { + interrupted_prior := Black; + BlinkingYellowTimeout3_prior := 0; + LightCommands_displayNone_Out_prior := true; + } + else { + if (((normal_prior == Red) && Control_toggle_In_prior)) { + if ((normal_prior == Red)) { + a_prior := true; + } + normal_prior := Green; + LightCommands_displayGreen_Out_prior := true; + } + else { + if (((normal_prior == Yellow) && Control_toggle_In_prior)) { + normal_prior := Red; + LightCommands_displayRed_Out_prior := true; + } + else { + if (((normal_prior == Green) && Control_toggle_In_prior)) { + b_prior := 4; + normal_prior := Yellow; + LightCommands_displayYellow_Out_prior := true; + } + } + } + } + } + } + } + PoliceInterrupt_police_In_prior := false; + Control_toggle_In_prior := false; + if (((main_region_second == Interrupted) && PoliceInterrupt_police_In_second)) { + interrupted_second := __Inactive__; + main_region_second := Normal; + if ((normal_second == __Inactive__)) { + normal_second := Red; + } + else { + normal_second := (if (normal_second == Red_Inactive_) then Red else (if (normal_second == Yellow_Inactive_) then Yellow else Green)); + } + if ((normal_second == Red)) { + LightCommands_displayRed_Out_second := true; + } + else { + if ((normal_second == Yellow)) { + LightCommands_displayYellow_Out_second := true; + } + else { + if ((normal_second == Green)) { + LightCommands_displayGreen_Out_second := true; + } + } + } + } + else { + if (((main_region_second == Normal) && PoliceInterrupt_police_In_second)) { + if ((main_region_second == Normal)) { + if ((normal_second == Red)) { + a_second := true; + } + asd_second := 321; + } + normal_second := (if (normal_second == Red) then Red_Inactive_ else (if (normal_second == Yellow) then Yellow_Inactive_ else Green_Inactive_)); + main_region_second := Interrupted; + interrupted_second := BlinkingYellow; + BlinkingYellowTimeout3_second := 0; + LightCommands_displayYellow_Out_second := true; + } + else { + if (((interrupted_second == Black) && (500 <= BlinkingYellowTimeout3_second))) { + interrupted_second := BlinkingYellow; + BlinkingYellowTimeout3_second := 0; + LightCommands_displayYellow_Out_second := true; + } + else { + if (((interrupted_second == BlinkingYellow) && (500 <= BlinkingYellowTimeout3_second))) { + interrupted_second := Black; + BlinkingYellowTimeout3_second := 0; + LightCommands_displayNone_Out_second := true; + } + else { + if (((normal_second == Red) && Control_toggle_In_second)) { + if ((normal_second == Red)) { + a_second := true; + } + normal_second := Green; + LightCommands_displayGreen_Out_second := true; + } + else { + if (((normal_second == Yellow) && Control_toggle_In_second)) { + normal_second := Red; + LightCommands_displayRed_Out_second := true; + } + else { + if (((normal_second == Green) && Control_toggle_In_second)) { + b_second := 4; + normal_second := Yellow; + LightCommands_displayYellow_Out_second := true; + } + } + } + } + } + } + } + Control_toggle_In_second := false; + PoliceInterrupt_police_In_second := false; + PoliceInterrupt_police_In_controller := false; +} +init { + InitTimeout3_controller := (2 * 1000); + main_region_controller := __Inactive__; + operating_controller := __Inactive__; + PoliceInterrupt_police_In_controller := false; + b_prior := 0; + a_prior := false; + asd_prior := 0; + BlinkingYellowTimeout3_prior := 500; + main_region_prior := __Inactive__; + interrupted_prior := __Inactive__; + normal_prior := __Inactive__; + PoliceInterrupt_police_In_prior := false; + Control_toggle_In_prior := false; + LightCommands_displayNone_Out_prior := false; + LightCommands_displayRed_Out_prior := false; + LightCommands_displayGreen_Out_prior := false; + LightCommands_displayYellow_Out_prior := false; + b_second := 0; + a_second := false; + asd_second := 0; + BlinkingYellowTimeout3_second := 500; + main_region_second := __Inactive__; + normal_second := __Inactive__; + interrupted_second := __Inactive__; + PoliceInterrupt_police_In_second := false; + Control_toggle_In_second := false; + LightCommands_displayGreen_Out_second := false; + LightCommands_displayNone_Out_second := false; + LightCommands_displayRed_Out_second := false; + LightCommands_displayYellow_Out_second := false; + main_region_controller := Operating; + operating_controller := Init; + main_region_prior := Normal; + normal_prior := Red; + main_region_second := Normal; + normal_second := Red; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + LightCommands_displayRed_Out_prior := true; + LightCommands_displayRed_Out_second := true; +} +env { + havoc PoliceInterrupt_police_In_controller; + LightCommands_displayYellow_Out_prior := false; + LightCommands_displayGreen_Out_prior := false; + LightCommands_displayNone_Out_prior := false; + LightCommands_displayRed_Out_prior := false; + LightCommands_displayRed_Out_second := false; + LightCommands_displayYellow_Out_second := false; + LightCommands_displayGreen_Out_second := false; + LightCommands_displayNone_Out_second := false; +} diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/Crossroad-Theta_timed.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/Crossroad-Theta_timed.xsts new file mode 100644 index 0000000000..22e81ed766 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/Crossroad-Theta_timed.xsts @@ -0,0 +1,324 @@ +type Main_region_Controller : { __Inactive__, Operating } +type Operating_Controller : { __Inactive__, Init, PriorityPrepares, Priority, Secondary, SecondaryPrepares, Init_Inactive_, PriorityPrepares_Inactive_, Priority_Inactive_, Secondary_Inactive_, SecondaryPrepares_Inactive_ } +type Main_region_TrafficLightCtrl : { __Inactive__, Interrupted, Normal } +type Interrupted_TrafficLightCtrl : { __Inactive__, Black, BlinkingYellow } +type Normal_TrafficLightCtrl : { __Inactive__, Red, Yellow, Green, Red_Inactive_, Yellow_Inactive_, Green_Inactive_ } +var PoliceInterrupt_police_In_controller : boolean = false +ctrl var main_region_controller : Main_region_Controller = __Inactive__ +ctrl var operating_controller : Operating_Controller = __Inactive__ +var InitTimeout3_controller : clock +var PoliceInterrupt_police_In_prior : boolean = false +var LightCommands_displayNone_Out_prior : boolean = false +var Control_toggle_In_prior : boolean = false +var LightCommands_displayRed_Out_prior : boolean = false +var LightCommands_displayGreen_Out_prior : boolean = false +var LightCommands_displayYellow_Out_prior : boolean = false +ctrl var main_region_prior : Main_region_TrafficLightCtrl = __Inactive__ +ctrl var interrupted_prior : Interrupted_TrafficLightCtrl = __Inactive__ +ctrl var normal_prior : Normal_TrafficLightCtrl = __Inactive__ +var asd_prior : integer = 0 +var b_prior : integer = 0 +var a_prior : boolean = false +var BlinkingYellowTimeout3_prior : clock +var LightCommands_displayGreen_Out_second : boolean = false +var PoliceInterrupt_police_In_second : boolean = false +var LightCommands_displayNone_Out_second : boolean = false +var LightCommands_displayRed_Out_second : boolean = false +var LightCommands_displayYellow_Out_second : boolean = false +var Control_toggle_In_second : boolean = false +ctrl var main_region_second : Main_region_TrafficLightCtrl = __Inactive__ +ctrl var normal_second : Normal_TrafficLightCtrl = __Inactive__ +ctrl var interrupted_second : Interrupted_TrafficLightCtrl = __Inactive__ +var asd_second : integer = 0 +var a_second : boolean = false +var b_second : integer = 0 +var BlinkingYellowTimeout3_second : clock + +trans { + __delay; + if (((main_region_controller == Operating) && PoliceInterrupt_police_In_controller)) { + operating_controller := (if (operating_controller == Init) then Init_Inactive_ else (if (operating_controller == PriorityPrepares) then PriorityPrepares_Inactive_ else (if (operating_controller == Priority) then Priority_Inactive_ else (if (operating_controller == Secondary) then Secondary_Inactive_ else SecondaryPrepares_Inactive_)))); + PoliceInterrupt_police_In_prior := true; + PoliceInterrupt_police_In_second := true; + main_region_controller := Operating; + if ((operating_controller == __Inactive__)) { + operating_controller := Init; + } + else { + operating_controller := (if (operating_controller == Init_Inactive_) then Init else (if (operating_controller == PriorityPrepares_Inactive_) then PriorityPrepares else (if (operating_controller == Priority_Inactive_) then Priority else (if (operating_controller == Secondary_Inactive_) then Secondary else SecondaryPrepares)))); + } + if ((operating_controller == Init)) { + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + } + else { + if ((operating_controller == PriorityPrepares)) { + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + } + else { + if ((operating_controller == Priority)) { + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + Control_toggle_In_second := true; + } + else { + if ((operating_controller == Secondary)) { + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + Control_toggle_In_second := true; + } + else { + if ((operating_controller == SecondaryPrepares)) { + InitTimeout3_controller := 0; + Control_toggle_In_second := true; + } + } + } + } + } + } + else { + if (((operating_controller == Init) && ((2 * 1000) <= InitTimeout3_controller))) { + operating_controller := PriorityPrepares; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + } + else { + if (((operating_controller == PriorityPrepares) && ((1 * 1000) <= InitTimeout3_controller))) { + operating_controller := Secondary; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + Control_toggle_In_second := true; + } + else { + if (((operating_controller == Priority) && ((2 * 1000) <= InitTimeout3_controller) && (true != false))) { + operating_controller := PriorityPrepares; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + } + else { + if (((operating_controller == Secondary) && ((2 * 1000) <= InitTimeout3_controller))) { + operating_controller := SecondaryPrepares; + InitTimeout3_controller := 0; + Control_toggle_In_second := true; + } + else { + if (((operating_controller == SecondaryPrepares) && ((1 * 1000) <= InitTimeout3_controller))) { + operating_controller := Priority; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + Control_toggle_In_second := true; + } + } + } + } + } + } + if (((main_region_prior == Interrupted) && PoliceInterrupt_police_In_prior)) { + interrupted_prior := __Inactive__; + main_region_prior := Normal; + if ((normal_prior == __Inactive__)) { + normal_prior := Red; + } + else { + normal_prior := (if (normal_prior == Red_Inactive_) then Red else (if (normal_prior == Yellow_Inactive_) then Yellow else Green)); + } + if ((normal_prior == Red)) { + LightCommands_displayRed_Out_prior := true; + } + else { + if ((normal_prior == Yellow)) { + LightCommands_displayYellow_Out_prior := true; + } + else { + if ((normal_prior == Green)) { + LightCommands_displayGreen_Out_prior := true; + } + } + } + } + else { + if (((main_region_prior == Normal) && PoliceInterrupt_police_In_prior)) { + if ((main_region_prior == Normal)) { + if ((normal_prior == Red)) { + a_prior := true; + } + asd_prior := 321; + } + normal_prior := (if (normal_prior == Red) then Red_Inactive_ else (if (normal_prior == Yellow) then Yellow_Inactive_ else Green_Inactive_)); + main_region_prior := Interrupted; + interrupted_prior := BlinkingYellow; + BlinkingYellowTimeout3_prior := 0; + LightCommands_displayYellow_Out_prior := true; + } + else { + if (((interrupted_prior == Black) && (500 <= BlinkingYellowTimeout3_prior))) { + interrupted_prior := BlinkingYellow; + BlinkingYellowTimeout3_prior := 0; + LightCommands_displayYellow_Out_prior := true; + } + else { + if (((interrupted_prior == BlinkingYellow) && (500 <= BlinkingYellowTimeout3_prior))) { + interrupted_prior := Black; + BlinkingYellowTimeout3_prior := 0; + LightCommands_displayNone_Out_prior := true; + } + else { + if (((normal_prior == Red) && Control_toggle_In_prior)) { + if ((normal_prior == Red)) { + a_prior := true; + } + normal_prior := Green; + LightCommands_displayGreen_Out_prior := true; + } + else { + if (((normal_prior == Yellow) && Control_toggle_In_prior)) { + normal_prior := Red; + LightCommands_displayRed_Out_prior := true; + } + else { + if (((normal_prior == Green) && Control_toggle_In_prior)) { + b_prior := 4; + normal_prior := Yellow; + LightCommands_displayYellow_Out_prior := true; + } + } + } + } + } + } + } + PoliceInterrupt_police_In_prior := false; + Control_toggle_In_prior := false; + if (((main_region_second == Interrupted) && PoliceInterrupt_police_In_second)) { + interrupted_second := __Inactive__; + main_region_second := Normal; + if ((normal_second == __Inactive__)) { + normal_second := Red; + } + else { + normal_second := (if (normal_second == Red_Inactive_) then Red else (if (normal_second == Yellow_Inactive_) then Yellow else Green)); + } + if ((normal_second == Red)) { + LightCommands_displayRed_Out_second := true; + } + else { + if ((normal_second == Yellow)) { + LightCommands_displayYellow_Out_second := true; + } + else { + if ((normal_second == Green)) { + LightCommands_displayGreen_Out_second := true; + } + } + } + } + else { + if (((main_region_second == Normal) && PoliceInterrupt_police_In_second)) { + if ((main_region_second == Normal)) { + if ((normal_second == Red)) { + a_second := true; + } + asd_second := 321; + } + normal_second := (if (normal_second == Red) then Red_Inactive_ else (if (normal_second == Yellow) then Yellow_Inactive_ else Green_Inactive_)); + main_region_second := Interrupted; + interrupted_second := BlinkingYellow; + BlinkingYellowTimeout3_second := 0; + LightCommands_displayYellow_Out_second := true; + } + else { + if (((interrupted_second == Black) && (500 <= BlinkingYellowTimeout3_second))) { + interrupted_second := BlinkingYellow; + BlinkingYellowTimeout3_second := 0; + LightCommands_displayYellow_Out_second := true; + } + else { + if (((interrupted_second == BlinkingYellow) && (500 <= BlinkingYellowTimeout3_second))) { + interrupted_second := Black; + BlinkingYellowTimeout3_second := 0; + LightCommands_displayNone_Out_second := true; + } + else { + if (((normal_second == Red) && Control_toggle_In_second)) { + if ((normal_second == Red)) { + a_second := true; + } + normal_second := Green; + LightCommands_displayGreen_Out_second := true; + } + else { + if (((normal_second == Yellow) && Control_toggle_In_second)) { + normal_second := Red; + LightCommands_displayRed_Out_second := true; + } + else { + if (((normal_second == Green) && Control_toggle_In_second)) { + b_second := 4; + normal_second := Yellow; + LightCommands_displayYellow_Out_second := true; + } + } + } + } + } + } + } + Control_toggle_In_second := false; + PoliceInterrupt_police_In_second := false; + PoliceInterrupt_police_In_controller := false; +} +init { + InitTimeout3_controller := (2 * 1000); + main_region_controller := __Inactive__; + operating_controller := __Inactive__; + PoliceInterrupt_police_In_controller := false; + b_prior := 0; + a_prior := false; + asd_prior := 0; + BlinkingYellowTimeout3_prior := 500; + main_region_prior := __Inactive__; + interrupted_prior := __Inactive__; + normal_prior := __Inactive__; + PoliceInterrupt_police_In_prior := false; + Control_toggle_In_prior := false; + LightCommands_displayNone_Out_prior := false; + LightCommands_displayRed_Out_prior := false; + LightCommands_displayGreen_Out_prior := false; + LightCommands_displayYellow_Out_prior := false; + b_second := 0; + a_second := false; + asd_second := 0; + BlinkingYellowTimeout3_second := 500; + main_region_second := __Inactive__; + normal_second := __Inactive__; + interrupted_second := __Inactive__; + PoliceInterrupt_police_In_second := false; + Control_toggle_In_second := false; + LightCommands_displayGreen_Out_second := false; + LightCommands_displayNone_Out_second := false; + LightCommands_displayRed_Out_second := false; + LightCommands_displayYellow_Out_second := false; + main_region_controller := Operating; + operating_controller := Init; + main_region_prior := Normal; + normal_prior := Red; + main_region_second := Normal; + normal_second := Red; + InitTimeout3_controller := 0; + Control_toggle_In_prior := true; + LightCommands_displayRed_Out_prior := true; + LightCommands_displayRed_Out_second := true; +} +env { + havoc PoliceInterrupt_police_In_controller; + LightCommands_displayYellow_Out_prior := false; + LightCommands_displayGreen_Out_prior := false; + LightCommands_displayNone_Out_prior := false; + LightCommands_displayRed_Out_prior := false; + LightCommands_displayRed_Out_second := false; + LightCommands_displayYellow_Out_second := false; + LightCommands_displayGreen_Out_second := false; + LightCommands_displayNone_Out_second := false; +} diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/clocks.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/clocks.xsts new file mode 100644 index 0000000000..d9d5ee009a --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/clocks.xsts @@ -0,0 +1,38 @@ +var a : integer = 0 +ctrl var b : integer = 10 +var c : boolean +var x : clock +var y : clock + +trans { + if (a < b-1) { + a := a+1; + b := b-1; + x := 0; + } else { + y := 0; + } +} or { + for i from 0 to b do { + a := b-1; + } +} or { + choice { + if (x < 10 || (y > 10 && b > a)) { + b := b+1; + x := 0; + y := 0; + } + } or { + c := (0 >= x - y); + b := 0; + } +} + +init { + __delay; +} + +env { + __delay; +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/xta_to_txsts.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/xta_to_txsts.xsts new file mode 100644 index 0000000000..5dcf08477a --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/xta_to_txsts.xsts @@ -0,0 +1,37 @@ +ctrl var L : integer = 0 +var x1 : integer = 0 +var x2 : integer = 0 +var c1 : clock +var c2 : clock + +trans { + assume L == 0; + x2 := 2; + c1 := 0; + L := 1; + __delay; +} or { + assume L == 1; + x1 := 1; + c2 := 0; + L := 2; + __delay; +} or { + assume L == 2; + c2 := 0; + __delay; +} or { + assume L == 2; + assume c1 < 1 && c2 >= 1; + x1 := x1 + 1; + __delay; +} or { + assume L == 2; + assume x1 > 1; + L := 3; + __delay; +} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival1.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival1.prop new file mode 100644 index 0000000000..3d12cda480 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival1.prop @@ -0,0 +1,3 @@ +prop { + !(__id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_0_Ervenytelen_0__coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival10.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival10.prop new file mode 100644 index 0000000000..d028b75b5a --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival10.prop @@ -0,0 +1,3 @@ +prop { + !(__id_Idozites_nem_fut_1_8_Ervenytelen_0__coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival2.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival2.prop new file mode 100644 index 0000000000..fc2ba4fa9d --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival2.prop @@ -0,0 +1,3 @@ +prop { + !(__id_Celoldas_idozites_fut_8_1_Oldas_4__coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival3.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival3.prop new file mode 100644 index 0000000000..bfe36468f6 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival3.prop @@ -0,0 +1,3 @@ +prop { + !(__id_Ervenytelen_0_2_Idozites_nem_fut_1__coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival4.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival4.prop new file mode 100644 index 0000000000..4891b1974e --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival4.prop @@ -0,0 +1,3 @@ +prop { + !(__id_Oldas_4_3_Celoldas_idozites_nem_fut_5__coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival5.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival5.prop new file mode 100644 index 0000000000..cd0fddb0d8 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival5.prop @@ -0,0 +1,3 @@ +prop { + !(__id_choice_6_in_main_region_of_bJbCOID_allapotgep_4_Celoldas_idozites_nem_fut_5__coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival6.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival6.prop new file mode 100644 index 0000000000..2a21c255f4 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival6.prop @@ -0,0 +1,3 @@ +prop { + !(__id_Celoldas_idozites_nem_fut_5_5_Celoldas_idozites_fut_8__coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival7.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival7.prop new file mode 100644 index 0000000000..cd463f3d02 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival7.prop @@ -0,0 +1,3 @@ +prop { + !(Fut_NemFut_coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival8.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival8.prop new file mode 100644 index 0000000000..61d6178dda --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival8.prop @@ -0,0 +1,3 @@ +prop { + !(__id_Tranziens_2_6_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5__coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival9.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival9.prop new file mode 100644 index 0000000000..a49c6ebe65 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival9.prop @@ -0,0 +1,3 @@ +prop { + !(__id_choice_6_in_region_1_in_Celoldas_idozites_nem_fut_5_7_Idozites_nem_fut_1__coid) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/antival_safety.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival_safety.prop new file mode 100644 index 0000000000..da0b8cf851 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/antival_safety.prop @@ -0,0 +1,13 @@ +prop { + !((main_region_of_mo_antivalchk_antival_chk_I_CR == Hibaallapot_8 + || main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_0_1 + || main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_1_2 + || main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_0_rol_1_re_3 + || main_region_of_mo_antivalchk_antival_chk_I_CR == Hibatarolassal_1_rol_0_ra_7) + && (main_region_of_mo_antivalchk_antival_chk_I_FT == Hibaallapot_8 + || main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_0_1 + || main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_1_2 + || main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_0_rol_1_re_3 + || main_region_of_mo_antivalchk_antival_chk_I_FT == Hibatarolassal_1_rol_0_ra_7) + && StateMachine_OutPort_O_COID_Out_O_COIDValue_coid == ACTIVE) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/clocks.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/clocks.prop new file mode 100644 index 0000000000..63e23da18f --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/clocks.prop @@ -0,0 +1,3 @@ +prop { + a <= b || b == 0; +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/crossroad_safety.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/crossroad_safety.prop new file mode 100644 index 0000000000..7bf8c22b99 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/crossroad_safety.prop @@ -0,0 +1,3 @@ +prop { + !(LightCommands_displayGreen_Out_prior && LightCommands_displayGreen_Out_second) +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/xta_to_txsts.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/xta_to_txsts.prop new file mode 100644 index 0000000000..ed6cec3fb2 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/xta_to_txsts.prop @@ -0,0 +1,3 @@ +prop{ + !(L == 3) +} \ No newline at end of file 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 index 9176084afd..07ac40ba92 100644 --- 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 @@ -27,6 +27,7 @@ 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.*; +import hu.bme.mit.theta.xsts.analysis.config.combined.XstsCombinedConfigBuilder; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; import hu.bme.mit.theta.xsts.pnml.PnmlParser; import hu.bme.mit.theta.xsts.pnml.PnmlToXSTS; @@ -102,6 +103,21 @@ public class XstsCli { @Parameter(names = {"--visualize"}, description = "Write proof or counterexample to file in dot format") String dotfile = null; + @Parameter(names = {"--clockreplacement"}, description = "Clock replacement type") + ClockImpl clockImpl = ClockImpl.RAT; + + @Parameter(names = {"--combined"}, description = "Run combined abstraction") + boolean combinedAlgorithm = false; + + @Parameter(names = {"--combinedsearch"}, description = "Search strategy for combined abstraction") + XstsCombinedConfigBuilder.Search combinedSearch = XstsCombinedConfigBuilder.Search.BFS; + + @Parameter(names = {"--clockstrategy"}, description = "Clock strategy for combined abstraction") + XstsCombinedConfigBuilder.ClockStrategy clockStrategy = XstsCombinedConfigBuilder.ClockStrategy.NONE; + + @Parameter(names = {"--zonerefinement"}, description = "Refinement strategy for zone states") + XstsCombinedConfigBuilder.ZoneRefinement zoneRefinement = XstsCombinedConfigBuilder.ZoneRefinement.BW_ITP; + private Logger logger; public XstsCli(final String[] args) { @@ -200,9 +216,18 @@ private XSTS loadModel() throws Exception { private XstsConfig buildConfiguration(final XSTS xsts) throws Exception { try { - return new XstsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) - .maxEnum(maxEnum).autoExpl(autoExpl).initPrec(initPrec).pruneStrategy(pruneStrategy) - .search(search).predSplit(predSplit).optimizeStmts(optimizeStmts).logger(logger).build(xsts); + if (combinedAlgorithm) { + return new XstsCombinedConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) + .maxEnum(maxEnum).autoExpl(autoExpl).initPrec(initPrec).pruneStrategy(pruneStrategy) + .search(combinedSearch).predSplit(predSplit).optimizeStmts(optimizeStmts) + .clockStrategy(clockStrategy).zoneRefinement(zoneRefinement) + .logger(logger).build(xsts); + } else { + return new XstsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) + .maxEnum(maxEnum).autoExpl(autoExpl).initPrec(initPrec).pruneStrategy(pruneStrategy) + .search(search).predSplit(predSplit).optimizeStmts(optimizeStmts).clockImpl(clockImpl) + .logger(logger).build(xsts); + } } catch (final Exception ex) { throw new Exception("Could not create configuration: " + ex.getMessage(), ex); }