diff --git a/doc/CEGAR-algorithms.md b/doc/CEGAR-algorithms.md index 632e31e774..54b422ff0d 100644 --- a/doc/CEGAR-algorithms.md +++ b/doc/CEGAR-algorithms.md @@ -8,7 +8,7 @@ This document gives a brief introduction to the possible configuration options o > "[Counterexample-Guided Abstraction Refinement](https://link.springer.com/chapter/10.1007/10722167_15) (CEGAR) is a widely used technique for the automated formal verification of different systems, including both software and hardware. CEGAR works by iteratively constructing and refining abstractions until a proper precision is reached. -It starts with computing an abstraction of the system with respect to some abstract domain and a given initial -- usually coarse -- precision. +It starts with computing an abstraction of the system with respect to some abstract dataDomain and a given initial -- usually coarse -- precision. The abstraction [over-approximates](https://dl.acm.org/doi/10.1145/186025.186051) the possible behaviors (i.e., the state space) of the original system. Thus, if no erroneous behavior can be found in the abstract state space then the original system is also safe. However, abstract counterexamples corresponding to erroneous behaviors must be checked whether they are reproducible (feasible) in the original system. @@ -28,18 +28,18 @@ Quoted from [Á. Hajdu and Z. Micskei - Efficient Strategies for CEGAR-Based Mod Note that not all options might be available in all tools. The available options, along with their default values are presented in the help screen (`--help`) of each tool. -### `--domain` +### `--dataDomain` -The domain controls the abstract information that is being tracked about the system. +The dataDomain controls the abstract information that is being tracked about the system. * `PRED_CART`: [Cartesian predicate abstraction](https://link.springer.com/article/10.1007/s10009-002-0095-0) keeps track of conjunctions of logical predicates (e.g., `x > 5 and y = x`) instead of concrete values. * `PRED_BOOL`: [Boolean predicate abstraction](https://link.springer.com/article/10.1007/s10009-002-0095-0) keeps track of arbitrary Boolean combination of predicates. * `PRED_SPLIT`: Boolean predicate abstraction, but states are [split]((https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf)) into sub-states along disjunctions. * `EXPL`: [Explicit-value abstraction]((https://link.springer.com/chapter/10.1007/978-3-642-37057-1_11)) keeps track of concrete values, but only for a (continuously expanded) set of variables. -* `EXPL_PRED_CART`, `EXPL_PRED_SPLIT`, `EXPL_PRED_BOOL` and `EXPL_PRED_COMBINED`: Product abstraction domains, available for XSTS models. The set of control variables (marked with `ctrl`) are tracked explicitly while others are tracked by predicates (using the corresponding predicate domain). Variables can automatically be switched from predicate tracking to explicit tracking depending on the `--autoexpl` option (see below). +* `EXPL_PRED_CART`, `EXPL_PRED_SPLIT`, `EXPL_PRED_BOOL` and `EXPL_PRED_COMBINED`: Product abstraction domains, available for XSTS models. The set of control variables (marked with `ctrl`) are tracked explicitly while others are tracked by predicates (using the corresponding predicate dataDomain). Variables can automatically be switched from predicate tracking to explicit tracking depending on the `--autoexpl` option (see below). -Predicate abstraction (`PRED_*`) tracks logical formulas instead of concrete values of variables, which can be efficient for variables with large (or infinite) domain. -Explicit-values (`EXPL`) keep track of a subset of system variables, which can be efficient if variables are mostly deterministic or have a small domain. +Predicate abstraction (`PRED_*`) tracks logical formulas instead of concrete values of variables, which can be efficient for variables with large (or infinite) dataDomain. +Explicit-values (`EXPL`) keep track of a subset of system variables, which can be efficient if variables are mostly deterministic or have a small dataDomain. Cartesian predicate abstraction only uses conjunctions (more efficient) while Boolean allows arbitrary formulas (more expressive). Boolean predicate abstraction often gives predicates in a disjunctive normal form (DNF). In `PRED_BOOL` this DNF formula is treated as a single state, while in `PRED_SPLIT` each operand of the disjunction is a separate state. @@ -54,10 +54,10 @@ More information on the abstract domains can be found in Section 2.2.1 and 3.1.3 Controls the initial precision of the abstraction (e.g., what predicates or variables are tracked initially). * `EMPTY`: Start with an empty initial precision. -* `ALLVARS`: Tracks all variables from the beginning. Available for CFA and XSTS if `--domain` is `EXPL`. -* `ALLASSUMES`: Track all assumptions by default (e.g., branch/loop conditions). Only applicable for CFA and if `--domain` is `PRED_*`. -* `PROP`: Available for XSTS. Tracks variables from the property if `--domain` is `EXPL` and predicates from the property if `--domain` is `PRED_*`. -* `CTRL`: Available for XSTS if `--domain` is `EXPL` or `EXPL_PRED_*`. Tracks all control variables. +* `ALLVARS`: Tracks all variables from the beginning. Available for CFA and XSTS if `--dataDomain` is `EXPL`. +* `ALLASSUMES`: Track all assumptions by default (e.g., branch/loop conditions). Only applicable for CFA and if `--dataDomain` is `PRED_*`. +* `PROP`: Available for XSTS. Tracks variables from the property if `--dataDomain` is `EXPL` and predicates from the property if `--dataDomain` is `PRED_*`. +* `CTRL`: Available for XSTS if `--dataDomain` is `EXPL` or `EXPL_PRED_*`. Tracks all control variables. We observed that usually the `EMPTY` initial precision yields good performance: the algorithm can automatically determine the precision. However, if the system is mostly deterministic, it might be suitable to track all variables from the beginning. @@ -84,14 +84,14 @@ Available for CFA, determines the [points where abstraction is applied](https:// ### `--maxenum` Available for CFA and XSTS. -Maximal number of states to be enumerated when performing explicit-value analysis (`--domain EXPL`) and an expression cannot be deterministically evaluated. +Maximal number of states to be enumerated when performing explicit-value analysis (`--dataDomain EXPL`) and an expression cannot be deterministically evaluated. If the limit is exceeded, unknown values are propagated. -As a special case, `0` stands for infinite, but it should only be used if the model does not have any variable with unbounded domain (or that variable is deterministically assigned). +As a special case, `0` stands for infinite, but it should only be used if the model does not have any variable with unbounded dataDomain (or that variable is deterministically assigned). In general, values between `5` to `50` perform well (see Section 3.1.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information). ### `--autoexpl` -Automatic predicate-to-explicit switching strategy. Available for XSTS, when used an `EXPL_PRED_*` domain. The goal of these options is to automatically detect when many values of a variable are enumerated in order to unroll a loop. +Automatic predicate-to-explicit switching strategy. Available for XSTS, when used an `EXPL_PRED_*` dataDomain. The goal of these options is to automatically detect when many values of a variable are enumerated in order to unroll a loop. * `STATIC`: No automatic switching * `NEWATOMS`: A variable is switched to explicit tracking when it appears in an atom that isn't present in the model. * `NEWOPERANDS`: A variable is switched to explicit tracking when it appears in an expression with an operand that it doesn't appear with in the model. @@ -104,7 +104,7 @@ Strategy for refining the precision of the abstraction, i.e., inferring new pred * `BW_BIN_ITP`: Backward binary interpolation (see Section 3.2.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information). Searches backwards for the first state where the counterexample becomes infeasible starting from the target state. * `SEQ_ITP`: Sequence interpolation. * `MULTI_SEQ`: Sequence interpolation with multiple counterexamples (see Section 3.2.2 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information). Can be useful for models with high cyclomatic complexity to converge faster. -* `UNSAT_CORE`: Extract variables to be tracked from an unsat core, only available if `--domain` is `EXPL`. +* `UNSAT_CORE`: Extract variables to be tracked from an unsat core, only available if `--dataDomain` is `EXPL`. * `UCB`: Extracts predicates or variables using weakest preconditions and unsat cores ([see paper](https://link.springer.com/chapter/10.1007%2F978-3-319-26287-1_10) for more information). _Experimental feature._ Available for CFA. * `NWT_*`: Newton-style refinement. _Experimental feature._ Available for CFA. The following variants are supported ([see paper](https://dl.acm.org/doi/10.1145/3106237.3106307) for more information): * `NWT_SP` and `NWT_WP` only works for really simple inputs, @@ -120,7 +120,7 @@ Floating point support *(known experimental problems)*: ### `--predsplit` -Available if `--domain` is `PRED_*`. +Available if `--dataDomain` is `PRED_*`. Determines whether splitting is applied to new predicates that are obtained during refinement. * `WHOLE`: Keep predicates as a whole, no splitting is applied. Can perform well if the model has many Boolean variables. * `CONJUNCTS`: Split predicates into conjuncts. diff --git a/doc/Portfolio.md b/doc/Portfolio.md index 59d204ef03..92e7b26d65 100644 --- a/doc/Portfolio.md +++ b/doc/Portfolio.md @@ -15,11 +15,11 @@ Usage of the portfolio simply happens by using the `--portfolio` flag with a par The complex portfolio has a global timeout of approximately 900 seconds. -"Based on preliminary experiments and domain knowledge, we manually constructed a dynamic algorithm selection portfolio for SV-COMP'22, illustrated by Figure. +"Based on preliminary experiments and dataDomain knowledge, we manually constructed a dynamic algorithm selection portfolio for SV-COMP'22, illustrated by Figure. Rounded white boxes correspond to decision points. We start by branching on the arithmetic (floats, bitvectors, integers). Under integers, there are further decision points based on the cyclomatic complexity and the number of havocs and variables. -Grey boxes represent configurations, defining the *solver\domain\refinement* in this order. +Grey boxes represent configurations, defining the *solver\dataDomain\refinement* in this order. Lighter and darker grey represents explicit and predicate domains respectively. Internal timeouts are written below the boxes. An unspecified timeout means that the configuration can use all the remaining time. @@ -42,9 +42,9 @@ The configurations are: 3. A Newtonian analysis (mainly to handle bitvector arithmetics as well) The precise parameters of these configurations: -1. `–domain EXPL –initprec EMPTY –search ERR –encodingLBE –refinement SEQ_ITP –maxenum 1 –precgranularityGLOBAL –prunestrategy LAZY` -2. `–domain PRED_CART –initprec EMPTY –search ERR–encoding LBE –refinement BW_BIN_ITP –predsplitWHOLE –precgranularity GLOBAL –prunestrategy LAZY` -3. `–domain EXPL –initprec EMPTY –search ERR –encoding LBE –refinement NWT_IT_WP –maxenum1 –precgranularity GLOBAL –prunestrategy LAZY` +1. `–dataDomain EXPL –initprec EMPTY –search ERR –encodingLBE –refinement SEQ_ITP –maxenum 1 –precgranularityGLOBAL –prunestrategy LAZY` +2. `–dataDomain PRED_CART –initprec EMPTY –search ERR–encoding LBE –refinement BW_BIN_ITP –predsplitWHOLE –precgranularity GLOBAL –prunestrategy LAZY` +3. `–dataDomain EXPL –initprec EMPTY –search ERR –encoding LBE –refinement NWT_IT_WP –maxenum1 –precgranularity GLOBAL –prunestrategy LAZY` ### Adding further portfolios To create a new concrete portfolio, create a subclass of the `hu.bme.mit.theta.xcfa.analysis.portfolio.common.AbstractPortfolio` class and implement its abstract method `executeAnalysis`. The `AbstractPortfolio` class serves as a utility, in which the execution of any given configuration with a time limit on a separate thread is already implemented in the method `executeConfiguration`. diff --git a/subprojects/cfa/cfa-analysis/README.md b/subprojects/cfa/cfa-analysis/README.md index 3442dd6ecb..9b85ddfdce 100644 --- a/subprojects/cfa/cfa-analysis/README.md +++ b/subprojects/cfa/cfa-analysis/README.md @@ -5,5 +5,5 @@ This project contains analysis modules related to the Control Flow Automata (CFA ### Related projects * [`analysis`](../../common/analysis/README.md): Common analysis modules. -* [`cfa`](../cfa/README.md): Classes to represent CFAs and a domain specific language (DSL) to parse CFAs from a textual representation. +* [`cfa`](../cfa/README.md): Classes to represent CFAs and a dataDomain specific language (DSL) to parse CFAs from a textual representation. * [`cfa-cli`](../cfa-cli/README.md): An executable tool (command line) for running analyses on CFAs. \ No newline at end of file diff --git a/subprojects/cfa/cfa-cli/README.md b/subprojects/cfa/cfa-cli/README.md index 8b9d53b38f..91c29c2248 100644 --- a/subprojects/cfa/cfa-cli/README.md +++ b/subprojects/cfa/cfa-cli/README.md @@ -6,7 +6,7 @@ For more information about the CFA formalism and its supported language elements ### Related projects -* [`cfa`](../cfa/README.md): Classes to represent CFAs and a domain specific language (DSL) to parse CFAs from a textual representation. +* [`cfa`](../cfa/README.md): Classes to represent CFAs and a dataDomain specific language (DSL) to parse CFAs from a textual representation. * [`cfa-analysis`](../cfa-analysis/README.md): CFA specific analysis modules enabling the algorithms to operate on them. ### Frontends diff --git a/subprojects/cfa/cfa/README.md b/subprojects/cfa/cfa/README.md index ec1c12891d..8e242a72d6 100644 --- a/subprojects/cfa/cfa/README.md +++ b/subprojects/cfa/cfa/README.md @@ -3,7 +3,7 @@ This project contains the Control Flow Automata (CFA) formalism. Its main purpose is to describe programs as a graphs, where nodes correspond to program locations and edges are annotated with program statements. The project contains: * Classes to represent CFAs. -* A domain specific language (DSL) to parse CFAs from a textual representation. +* A dataDomain specific language (DSL) to parse CFAs from a textual representation. ### Related projects diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ItpRefutation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ItpRefutation.java index 3763b6e806..d564045aed 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ItpRefutation.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ItpRefutation.java @@ -22,6 +22,7 @@ import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; import java.util.ArrayList; +import java.util.Collections; import java.util.Iterator; import java.util.List; import java.util.stream.Stream; @@ -55,6 +56,11 @@ private ItpRefutation(final List> itpSequence) { assert 0 <= this.pruneIndex && this.pruneIndex < itpSequence.size(); } + private ItpRefutation() { + itpSequence = Collections.emptyList(); + pruneIndex = -1; + } + public static ItpRefutation sequence(final List> itpSequence) { return new ItpRefutation(itpSequence); } @@ -115,4 +121,8 @@ public VarsRefutation toVarSetsRefutation() { } return VarsRefutation.create(builder.build()); } + + public static ItpRefutation emptyRefutation(){ + return new ItpRefutation(); + } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/Prod2Refutation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/Prod2Refutation.java new file mode 100644 index 0000000000..225f76278e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/Prod2Refutation.java @@ -0,0 +1,27 @@ +package hu.bme.mit.theta.analysis.expr.refinement; + +public class Prod2Refutation implements Refutation{ + + final private R1 refutation1; + final private R2 refutation2; + + public Prod2Refutation(R1 refutation1, R2 refutation2) { + this.refutation1 = refutation1; + this.refutation2 = refutation2; + } + + public R1 getRefutation1() { + return refutation1; + } + + public R2 getRefutation2() { + return refutation2; + } + + @Override + public int getPruneIndex() { + if(refutation1.getPruneIndex() < 0) return refutation2.getPruneIndex(); + if(refutation2.getPruneIndex() < 0) return refutation1.getPruneIndex(); + return refutation1.getPruneIndex() > refutation2.getPruneIndex() ? refutation2.getPruneIndex() : refutation1.getPruneIndex(); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/Refutation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/Refutation.java index 2f79efbf50..9ca996d356 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/Refutation.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/Refutation.java @@ -16,5 +16,8 @@ package hu.bme.mit.theta.analysis.expr.refinement; public interface Refutation { + int getPruneIndex(); + + } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ZoneRefutation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ZoneRefutation.java new file mode 100644 index 0000000000..34983e5d4e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ZoneRefutation.java @@ -0,0 +1,61 @@ +package hu.bme.mit.theta.analysis.expr.refinement; + +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.analysis.zone.DBM; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.rattype.RatType; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +public class ZoneRefutation implements Refutation{ + + private final int pruneIndex; + private final List zoneSequence; + private final List> clocks; + + + private ZoneRefutation(){ + pruneIndex = -1; + zoneSequence = Collections.emptyList(); + clocks = Collections.emptyList(); + } + private ZoneRefutation(int prunIndex, List zoneSequence, List> clocks) { + this.pruneIndex = prunIndex; + this.zoneSequence= ImmutableList.copyOf(zoneSequence); + this.clocks = clocks; + } + + public static ZoneRefutation binary(final int pruneIndex, final ZoneState itpZone, List> clocks, final int statecount) + { + final List zoneSequence = new ArrayList<>(); + for (int i = 0; i < statecount; i ++){ + if(i < pruneIndex) { + zoneSequence.add(ZoneState.top()); + } + else if( i == pruneIndex){ + zoneSequence.add(itpZone); + } + else zoneSequence.add(ZoneState.bottom()); + } + return new ZoneRefutation(pruneIndex, zoneSequence, clocks); + } + @Override + public int getPruneIndex() { + return this.pruneIndex; + } + + public ZoneState get(int index){ + return zoneSequence.get(index); + } + + public List> getClocks() { + return clocks; + } + + public static ZoneRefutation emptyRefutation(){ + return new ZoneRefutation(); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BasicDbm.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BasicDbm.java index 1de3039abe..a753376e60 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BasicDbm.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/BasicDbm.java @@ -123,7 +123,6 @@ public void up() { assert isClosed(); } } - //TODO miért? public void down() { if (isConsistent()) { for (int i = 1; i <= nClocks; i++) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ClockPredPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ClockPredPrec.java new file mode 100644 index 0000000000..8615b31377 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ClockPredPrec.java @@ -0,0 +1,126 @@ +package hu.bme.mit.theta.analysis.zone; + +import com.google.common.collect.ImmutableSet; +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.rattype.RatType; + +import java.util.*; +import java.util.stream.Collectors; + +import static com.google.common.base.Preconditions.checkNotNull; + +public class ClockPredPrec implements Prec{ + + private final Map, VarDecl>, Set> map; + private final Set> clocks; + + private ClockPredPrec(final Map, VarDecl>, Set> map, final Collection> clocks){ + checkNotNull(clocks); + this.clocks = ImmutableSet.copyOf(clocks); + this.map = map; + sort(); + } + + + public static ClockPredPrec of(final Collection> clocks) { + return ClockPredPrec.emptyPrec(clocks); + } + + + public static ClockPredPrec emptyPrec(final Collection> clocks){ + Map, VarDecl>, Set> empty = new HashMap<>(); + return new ClockPredPrec(empty, clocks); + } + + public Set> getVars() { + return clocks; + } + @Override + public String toString() { + return Utils.lispStringBuilder(getClass().getSimpleName()).addAll(clocks).toString(); + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) { + return true; + } else if (obj instanceof ClockPredPrec) { + final ClockPredPrec that = (ClockPredPrec) obj; + return this.getVars().equals(that.getVars()); + } else { + return false; + } + } + + public Collection> getUsedVars() { // This could be way more elegant + return clocks.stream().map(ratTypeVarDecl -> (VarDecl) ratTypeVarDecl).collect(Collectors.toSet()); + } + @Override + public int hashCode() { + return 31 * clocks.hashCode(); + } + + + + public static ClockPredPrec of(final Map, VarDecl>, Set> map, final Collection> clocks) { + //checknotnull + return new ClockPredPrec(map, clocks); + } + + + + public ClockPredPrec join(final ClockPredPrec other){ + //addClocks(other.getVars()); + for(Map.Entry, VarDecl>, Set> entry: other.map.entrySet()){ + if(map.containsKey(entry.getKey())){ + map.get(entry.getKey()).addAll(entry.getValue()); + } + else{ + map.put(entry.getKey(), entry.getValue()); + } + } + + sort(); + return this; + } + + @Override + public Prec join(Prec other) { + if(this == other)return this; + if(other instanceof ClockPredPrec other1){ + return join(other1); + } + else{ + throw new IllegalArgumentException(); + } + } + public Map, VarDecl>, Set> getPreds(){ + sort(); return map; + } + + + private void sort(){ + for (Pair, VarDecl> k: map.keySet()){ + map.get(k).stream().sorted(); + } + } + + public void add(VarDecl x, Integer b){ + Pair,VarDecl> key = new Pair<>(x); + if(!map.containsKey(key)){ + map.put(key, new HashSet()); + } + map.get(key).add(b); + + } + public void add(VarDecl x, VarDecl y,Integer b){ + Pair,VarDecl> key = new Pair<>(x,y); + if(!map.containsKey(key)){ + map.put(key, new HashSet()); + } + map.get(key).add(b); + + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java index 22833f5ac8..f2f06872f6 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java @@ -62,10 +62,12 @@ import hu.bme.mit.theta.core.clock.op.GuardOp; import hu.bme.mit.theta.core.clock.op.ResetOp; import hu.bme.mit.theta.core.clock.op.ShiftOp; +import hu.bme.mit.theta.core.decl.ParamDecl; import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.inttype.IntGeqExpr; import hu.bme.mit.theta.core.type.rattype.RatType; -final class DBM { +public class DBM { private static final IntBinaryOperator ZERO_DBM_VALUES = (x, y) -> Leq(0); private static final IntBinaryOperator TOP_DBM_VALUES = BasicDbm::defaultBound; @@ -836,4 +838,52 @@ private interface Procedure { void execute(); } + public void setIfGreater(ClockPredPrec prec){ + BasicDbm newdbm = new BasicDbm(dbm); + newdbm.free(); + ArrayList> changes = new ArrayList>(); + for (Pair, VarDecl> e : prec.getPreds().keySet()){ + + int i = signature.indexOf(e.getKey()); + int j; + + if(e.NoValue()){ + j = 0; + } + else j = signature.indexOf(e.getValue()); + int currval = dbm.get(i,j); + changes.add(new Pair(i,j)); + //its already sorted + var ps = new ArrayList<>(prec.getPreds().get(e)); + ps.add(DiffBounds.Inf()); + for(Integer b: ps) { + if( b >= currval){ + newdbm.set(i, j, b); + break; + } + +// if (DiffBounds.isStrict(b)) { +// if (DiffBounds.getBound(b) > DiffBounds.getBound(currval)) { +// +// } +// } else { +// if (DiffBounds.getBound(b) >= DiffBounds.getBound(currval)) { +// newdbm.set(i, j, b); +// break; +// } +// } + } + //if(newdbm.get(i,j) == dbm.get(i,j)) newdbm.set(i,j, DiffBounds.Inf()); + dbm.set(i,j,newdbm.get(i,j)); + } + for(int i = 0; i < dbm.size(); i++){ + for(int j = 1; j < dbm.size(); j++){ + dbm.set(i,j,newdbm.get(i,j)); + } + } + } + + + + } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DiffBounds.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DiffBounds.java index 2a06e50e36..6be5430704 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DiffBounds.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DiffBounds.java @@ -23,7 +23,7 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.rattype.RatType; -final class DiffBounds { +/*final*/ public class DiffBounds { private static final int INF = Integer.MAX_VALUE; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/Pair.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/Pair.java new file mode 100644 index 0000000000..41ba685252 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/Pair.java @@ -0,0 +1,54 @@ +package hu.bme.mit.theta.analysis.zone; + +import java.util.Objects; +import java.util.Optional; + +public class Pair { + private K key; + private Optional value; + + + public Pair(K key){ + this.key = key; + this.value = Optional.empty(); + } + public Pair(K key, V value){ + this.key = key; + this.value = Optional.of(value); + } + public K getKey(){ + return this.key; + } + public V getValue(){ + return this.value.get(); + } + + public boolean NoValue(){ return value.isEmpty();} + + public boolean equals(Pair p){ + if(key.equals(p.key)){ + if(value.isEmpty()) { + if(p.value.isEmpty()) return true; + else return false; + } + else{ + if(p.value.isEmpty()) return false; + else if(value.get().equals(p.value.get())) return true; + } + } + return false; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + + return equals((Pair)o); + } + + @Override + public int hashCode() { + return Objects.hash(key, value); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java index 596c795095..b80fc4f949 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java @@ -27,11 +27,11 @@ import static com.google.common.base.Preconditions.checkNotNull; -public final class ZonePrec implements Prec { +public class ZonePrec implements Prec { private final Set> clocks; - private ZonePrec(final Collection> clocks) { + protected ZonePrec(final Collection> clocks) { checkNotNull(clocks); this.clocks = ImmutableSet.copyOf(clocks); } @@ -70,6 +70,7 @@ public int hashCode() { public Collection> getUsedVars() { // This could be way more elegant return clocks.stream().map(ratTypeVarDecl -> (VarDecl) ratTypeVarDecl).collect(Collectors.toSet()); } + /////???? @Override public Prec join(Prec other) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java index a337e506b0..cfed6d7aba 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java @@ -222,6 +222,7 @@ public String toString() { return Utils.lispStringBuilder(getClass().getSimpleName()).aligned().addAll(constrs).toString(); } + //////// public static class Builder { @@ -300,4 +301,11 @@ public Builder norm(final Map, ? extends Integer> cei } } + public void clockPredicate(ClockPredPrec prec){ + dbm.setIfGreater(prec); + } + + public DBM getDbm() { + return dbm; + } } diff --git a/subprojects/sts/sts-analysis/README.md b/subprojects/sts/sts-analysis/README.md index edaaf61e9f..f58a550ff4 100644 --- a/subprojects/sts/sts-analysis/README.md +++ b/subprojects/sts/sts-analysis/README.md @@ -5,5 +5,5 @@ This project contains analysis modules related to the Symbolic Transition System ### Related projects * [`analysis`](../../common/analysis/README.md): Common analysis modules. -* [`sts`](../sts/README.md): Classes to represent STSs and a domain specific language (DSL) to parse STSs from a textual representation. +* [`sts`](../sts/README.md): Classes to represent STSs and a dataDomain specific language (DSL) to parse STSs from a textual representation. * [`sts-cli`](../sts-cli/README.md): An executable tool (command line) for running analyses on STSs. \ No newline at end of file diff --git a/subprojects/sts/sts-cli/README.md b/subprojects/sts/sts-cli/README.md index a5e2dbe130..db862a3eeb 100644 --- a/subprojects/sts/sts-cli/README.md +++ b/subprojects/sts/sts-cli/README.md @@ -5,7 +5,7 @@ For more information about the STS formalism and its supported language elements ### Related projects -* [`sts`](../sts/README.md): Classes to represent STSs and a domain specific language (DSL) to parse STSs from a textual representation. +* [`sts`](../sts/README.md): Classes to represent STSs and a dataDomain specific language (DSL) to parse STSs from a textual representation. * [`sts-analysis`](../sts-analysis/README.md): STS specific analysis modules enabling the algorithms to operate on them. ## Using the tool diff --git a/subprojects/sts/sts/README.md b/subprojects/sts/sts/README.md index d5ab271e82..09ee3c8fe6 100644 --- a/subprojects/sts/sts/README.md +++ b/subprojects/sts/sts/README.md @@ -4,7 +4,7 @@ This project contains the Symbolic Transition System (STS) formalism. It is a generic, low-level formalism that can describe any kind of system using variables and initial/transition expressions. The project includes: * Classes to represent STSs. -* A domain specific language (DSL) to parse STSs from a textual representation. +* A dataDomain specific language (DSL) to parse STSs from a textual representation. * A frontend that can parse systems described in the [AIGER](http://fmv.jku.at/aiger/) (And-Inverter Graph) format and represent them using STSs. ### Related projects diff --git a/subprojects/xcfa/xcfa/README.md b/subprojects/xcfa/xcfa/README.md index eec19ec721..f26e11eea2 100644 --- a/subprojects/xcfa/xcfa/README.md +++ b/subprojects/xcfa/xcfa/README.md @@ -7,7 +7,7 @@ groups of graphs, where edges are annotated with program statements and each gra single process. The project contains: * Classes to represent XCFAs. -* A domain specific language (DSL) to parse XCFAs from a textual representation. +* A dataDomain specific language (DSL) to parse XCFAs from a textual representation. * A program transformation method that takes LLVM IR and creates an XCFA. Every _XCFA_ model consists of global variables and _XcfaProcess_ definitions. _XcfaProcesses_ consist of thread-local variables and _XcfaProcedure_ definitions. _XcfaProcedures_ are akin to the _CFA_ models, in the sense that they consist of local variables, _XcfaLocations_ and _XcfaEdges_; and _XcfaEdges_ contain zero or more _XcfaLabels_. diff --git a/subprojects/xsts/xsts-analysis/README.md b/subprojects/xsts/xsts-analysis/README.md index 4ff1faedcd..1ab52dc713 100644 --- a/subprojects/xsts/xsts-analysis/README.md +++ b/subprojects/xsts/xsts-analysis/README.md @@ -5,5 +5,5 @@ This project contains analysis modules related to the Extended Symbolic Transiti ### Related projects * [`analysis`](../../common/analysis/README.md): Common analysis modules. -* [`xsts`](../xsts/README.md): Classes to represent XSTSs and a domain specific language (DSL) to parse XSTSs from a textual representation. +* [`xsts`](../xsts/README.md): Classes to represent XSTSs and a dataDomain specific language (DSL) to parse XSTSs from a textual representation. * [`xsts-cli`](../xsts-cli/README.md): An executable tool (command line) for running analyses on XSTSs. \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/README.md b/subprojects/xsts/xsts-cli/README.md index b85e272024..44b4300d5b 100644 --- a/subprojects/xsts/xsts-cli/README.md +++ b/subprojects/xsts/xsts-cli/README.md @@ -5,7 +5,7 @@ For more information about the XSTS formalism and its supported language element ### Related projects -* [`xsts`](../xsts/README.md): Classes to represent XSTSs and a domain specific language (DSL) to parse XSTSs from a textual representation. +* [`xsts`](../xsts/README.md): Classes to represent XSTSs and a dataDomain specific language (DSL) to parse XSTSs from a textual representation. * [`xsts-analysis`](../xsts-analysis/README.md): XSTS specific analysis modules enabling the algorithms to operate on them. ### Frontends diff --git a/subprojects/xsts/xsts/README.md b/subprojects/xsts/xsts/README.md index 2ff7b83f60..82f4a4ee51 100644 --- a/subprojects/xsts/xsts/README.md +++ b/subprojects/xsts/xsts/README.md @@ -3,7 +3,7 @@ This project contains the Extended Symbolic Transition System (XSTS) formalism. The project includes: * Classes to represent XSTSs. -* A domain specific language (DSL) to parse XSTSs from a textual representation. +* A dataDomain specific language (DSL) to parse XSTSs from a textual representation. * A frontend that can parse Petri net models described in the [PNML](http://www.pnml.org/) format (experimental). ### Related projects diff --git a/subprojects/xta/xta-analysis/README.md b/subprojects/xta/xta-analysis/README.md index 697b750d50..37cf0af214 100644 --- a/subprojects/xta/xta-analysis/README.md +++ b/subprojects/xta/xta-analysis/README.md @@ -5,5 +5,5 @@ This project contains analysis modules related to the Uppaal Timed Automata (XTA ### Related projects * [`analysis`](../../common/analysis/README.md): Common analysis modules. -* [`xta`](../xta/README.md): Classes to represent XTAs and a domain specific language (DSL) to parse XTAs from a textual representation. +* [`xta`](../xta/README.md): Classes to represent XTAs and a dataDomain specific language (DSL) to parse XTAs from a textual representation. * [`xta-cli`](../xta-cli/README.md): An executable tool (command line) for running analyses on XTAs. \ No newline at end of file diff --git a/subprojects/xta/xta-analysis/build.gradle.kts b/subprojects/xta/xta-analysis/build.gradle.kts index 3cdbc36fea..88df389b6f 100644 --- a/subprojects/xta/xta-analysis/build.gradle.kts +++ b/subprojects/xta/xta-analysis/build.gradle.kts @@ -13,4 +13,5 @@ dependencies { testImplementation(project(":theta-solver-z3")) testImplementation(project(":theta-solver")) implementation(project(":theta-solver-smtlib")) + } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockAnalysis.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockAnalysis.java new file mode 100644 index 0000000000..7692e05fc7 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockAnalysis.java @@ -0,0 +1,14 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import hu.bme.mit.theta.analysis.*; +import hu.bme.mit.theta.analysis.zone.ZonePrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.xta.analysis.XtaAction; + +public abstract class ClockAnalysis

implements Analysis { + + public abstract PartialOrd getPartialOrd(); + public abstract InitFunc getInitFunc(); + + public abstract TransFunc getTransFunc(); +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredAnalysis.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredAnalysis.java new file mode 100644 index 0000000000..0413381304 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredAnalysis.java @@ -0,0 +1,37 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +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.zone.ClockPredPrec; +import hu.bme.mit.theta.analysis.zone.ZoneOrd; +import hu.bme.mit.theta.analysis.zone.ZonePrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.xta.analysis.XtaAction; + +import java.time.Clock; + +public class ClockPredAnalysis implements Analysis { + + private static final ClockPredAnalysis INSTANCE = new ClockPredAnalysis(); + + private ClockPredAnalysis(){ + + } + public static ClockPredAnalysis getInstance(){return INSTANCE;} + @Override + public PartialOrd getPartialOrd() { + return ZoneOrd.getInstance(); + } + + @Override + public InitFunc getInitFunc() { + return ClockPredInitFunc.getInstance(); + } + + @Override + public TransFunc getTransFunc() { + return ClockPredTransFunc.getInstance(); + } +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredInitFunc.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredInitFunc.java new file mode 100644 index 0000000000..93c8af881c --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredInitFunc.java @@ -0,0 +1,25 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import hu.bme.mit.theta.analysis.InitFunc; +import hu.bme.mit.theta.analysis.zone.ClockPredPrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; + +import java.util.Collection; +import java.util.Collections; + +import static com.google.common.base.Preconditions.checkNotNull; + +public class ClockPredInitFunc implements InitFunc { + + + private static ClockPredInitFunc INSTANCE = new ClockPredInitFunc(); + private ClockPredInitFunc(){} + + static ClockPredInitFunc getInstance(){ return INSTANCE;} + @Override + public Collection getInitStates(ClockPredPrec prec) + { + checkNotNull(prec); + return Collections.singleton(ZoneState.zero(prec.getVars()).transform().up().build()); + } +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredOrd.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredOrd.java new file mode 100644 index 0000000000..535d987fd2 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredOrd.java @@ -0,0 +1,13 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import hu.bme.mit.theta.analysis.PartialOrd; +import hu.bme.mit.theta.analysis.zone.ZoneState; + +public class ClockPredOrd implements PartialOrd { + + + @Override + public boolean isLeq(ClockPredState state1, ClockPredState state2) { + return state1.isLeq(state2); + } +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredState.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredState.java new file mode 100644 index 0000000000..b57d307912 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredState.java @@ -0,0 +1,36 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import com.google.common.collect.ImmutableSet; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.rattype.RatType; + +import java.util.Collection; + +public class ClockPredState implements ExprState { + + private final Collection> clocks; + + //private final ZoneState zoneState; + + private ClockPredState(final Collection> clocks){ + this.clocks = ImmutableSet.copyOf(clocks); + + } + @Override + public boolean isBottom() { + return false; + } + + @Override + public Expr toExpr() { + return null; + } + public boolean isLeq(ClockPredState state1){ + if(clocks.contains(state1.clocks) && clocks.size() >= state1.clocks.size()) return true; + return false; + } +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java new file mode 100644 index 0000000000..cd8a0caada --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java @@ -0,0 +1,28 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.analysis.TransFunc; +import hu.bme.mit.theta.analysis.zone.ClockPredPrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.xta.analysis.XtaAction; + + +import java.util.Collection; + +public class ClockPredTransFunc implements TransFunc { + + private final static ClockPredTransFunc INSTANCE = new ClockPredTransFunc(); + private ClockPredTransFunc(){} + + static ClockPredTransFunc getInstance(){return INSTANCE;} + public Collection getSuccStates(ZoneState state, XtaAction action, ClockPredPrec prec) { + + ZoneState succState = XtaClockPredUtils.post(state, action, prec); + + + //ne legyen x-y inf + succState.clockPredicate(prec); +//új változó debughoz + return ImmutableList.of(succState); + } +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2ExplClockPredPrec.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2ExplClockPredPrec.java new file mode 100644 index 0000000000..f85352e33e --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2ExplClockPredPrec.java @@ -0,0 +1,63 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import hu.bme.mit.theta.analysis.expl.ExplPrec; +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; +import hu.bme.mit.theta.analysis.expr.refinement.Prod2Refutation; +import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; +import hu.bme.mit.theta.analysis.expr.refinement.ZoneRefutation; +import hu.bme.mit.theta.analysis.prod2.Prod2Prec; +import hu.bme.mit.theta.analysis.zone.ClockPredPrec; +import hu.bme.mit.theta.analysis.zone.*; +import hu.bme.mit.theta.core.clock.constr.ClockConstr; +import hu.bme.mit.theta.core.clock.constr.DiffLeqConstr; +import hu.bme.mit.theta.core.clock.constr.DiffLtConstr; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.utils.ExprUtils; + +import java.util.Collection; +import java.util.Iterator; + +import static com.google.common.base.Preconditions.checkNotNull; + +public class Prod2RefToProd2ExplClockPredPrec implements RefutationToPrec, Prod2Refutation> { + + + @Override + public Prod2Prec toPrec(Prod2Refutation refutation, int index) { + ClockPredPrec clockPredPrec = ClockPredPrec.emptyPrec(refutation.getRefutation2().getClocks()); + ExplPrec explPrec = ExplPrec.empty(); + if(refutation.getRefutation2().getPruneIndex()>=0) { + final ZoneState zone = refutation.getRefutation2().get(index); + if (!(zone.isBottom() || zone.isTop())) { + Iterator iterator = zone.getDbm().getConstrs().iterator(); + while (iterator.hasNext()) { + ClockConstr constr = iterator.next(); + + if (constr instanceof DiffLtConstr ltconstr) { + clockPredPrec.add(ltconstr.getLeftVar(), ltconstr.getRightVar(), DiffBounds.Lt(ltconstr.getBound())); + } else if (constr instanceof DiffLeqConstr leqconstr) { + clockPredPrec.add(leqconstr.getLeftVar(), leqconstr.getRightVar(), DiffBounds.Leq(leqconstr.getBound())); + } + } + } + } + if(refutation.getRefutation1().getPruneIndex()>=0) { + final Expr expr = refutation.getRefutation1().get(index); + final Collection> vars = ExprUtils.getVars(expr); + explPrec = ExplPrec.of(vars); + } + return Prod2Prec.of(explPrec,clockPredPrec); + + + } + + + @Override + public Prod2Prec join(Prod2Prec prec1, Prod2Prec prec2) { + checkNotNull(prec1.getPrec1()); + checkNotNull(prec2.getPrec1()); + return Prod2Prec.of(prec1.getPrec1().join(prec2.getPrec1()), prec1.getPrec2().join(prec2.getPrec2()) ); + } +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2PredClockPredPrec.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2PredClockPredPrec.java new file mode 100644 index 0000000000..2372f8a9bc --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2PredClockPredPrec.java @@ -0,0 +1,68 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; +import hu.bme.mit.theta.analysis.expr.refinement.Prod2Refutation; +import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; +import hu.bme.mit.theta.analysis.expr.refinement.ZoneRefutation; +import hu.bme.mit.theta.analysis.pred.ExprSplitters; +import hu.bme.mit.theta.analysis.pred.PredPrec; +import hu.bme.mit.theta.analysis.prod2.Prod2Prec; +import hu.bme.mit.theta.analysis.zone.ClockPredPrec; +import hu.bme.mit.theta.analysis.zone.DiffBounds; +import hu.bme.mit.theta.analysis.zone.ZonePrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.core.clock.constr.ClockConstr; +import hu.bme.mit.theta.core.clock.constr.DiffLeqConstr; +import hu.bme.mit.theta.core.clock.constr.DiffLtConstr; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; + +import java.util.Collections; +import java.util.Iterator; +import java.util.stream.Collectors; + +import static com.google.common.base.Preconditions.checkNotNull; + +public class Prod2RefToProd2PredClockPredPrec implements RefutationToPrec, Prod2Refutation> { + + private final ExprSplitters.ExprSplitter exprSplitter; + + public Prod2RefToProd2PredClockPredPrec(final ExprSplitters.ExprSplitter _splitter){ + exprSplitter = checkNotNull(_splitter); + } + @Override + public Prod2Prec toPrec(Prod2Refutation refutation, int index) { + ClockPredPrec clockPredPrec = ClockPredPrec.emptyPrec(refutation.getRefutation2().getClocks()); + PredPrec predPrec = PredPrec.of(); + if(refutation.getRefutation2().getPruneIndex() >= 0) { + final ZoneState zone = refutation.getRefutation2().get(index); + if (!(zone.isBottom() || zone.isTop())) { + Iterator iterator = zone.getDbm().getConstrs().iterator(); + while (iterator.hasNext()) { + ClockConstr constr = iterator.next(); + + if (constr instanceof DiffLtConstr ltconstr) { + clockPredPrec.add(ltconstr.getLeftVar(), ltconstr.getRightVar(), DiffBounds.Lt(ltconstr.getBound())); + } else if (constr instanceof DiffLeqConstr leqconstr) { + clockPredPrec.add(leqconstr.getLeftVar(), leqconstr.getRightVar(), DiffBounds.Leq(leqconstr.getBound())); + } + } + } + } + if(refutation.getRefutation1().getPruneIndex() >= 0) { + final Expr refExpr = refutation.getRefutation1().get(index); + + final var predSelectedExprs = exprSplitter.apply(refExpr).stream() + .collect(Collectors.toSet()); + predPrec = PredPrec.of(predSelectedExprs); + } + return Prod2Prec.of(predPrec, clockPredPrec); + + + } + + @Override + public Prod2Prec join(Prod2Prec prec1, Prod2Prec prec2) { + return (Prod2Prec)prec1.join(prec2); + } +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java new file mode 100644 index 0000000000..59f9024b84 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java @@ -0,0 +1,137 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.algorithm.ARG; +import hu.bme.mit.theta.analysis.algorithm.ArgEdge; +import hu.bme.mit.theta.analysis.algorithm.ArgNode; +import hu.bme.mit.theta.analysis.algorithm.ArgTrace; +import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult; +import hu.bme.mit.theta.analysis.algorithm.runtimecheck.ArgCexCheckHandler; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.expr.refinement.*; +import hu.bme.mit.theta.analysis.prod2.Prod2Prec; +import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.analysis.zone.ClockPredPrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.xta.analysis.XtaAction; +import hu.bme.mit.theta.xta.analysis.XtaState; +import hu.bme.mit.theta.xta.analysis.prec.XtaPrec; + +import java.util.List; +import java.util.Optional; +import java.util.stream.Collectors; + +import static com.google.common.base.Preconditions.checkNotNull; +import static java.util.stream.Collectors.toList; + +public final class SingleXtaTraceRefiner + implements Refiner>, XtaAction, XtaPrec>> +{ + + private final XtaTraceChecker zoneTraceChecker; + + private final ExprTraceChecker exprTraceChecker; + private final PrecRefiner>, XtaAction, XtaPrec>, Prod2Refutation> precRefiner; + private final PruneStrategy pruneStrategy; + private final Logger logger; + + private final R emptyRefutation; + + + + private SingleXtaTraceRefiner(XtaTraceChecker zoneTraceChecker, + ExprTraceChecker exprTraceChecker, + PrecRefiner>, + XtaAction, XtaPrec>, Prod2Refutation> precRefiner, + PruneStrategy pruneStrategy, Logger logger, R emptyRefutation) { + this.zoneTraceChecker = zoneTraceChecker; + this.exprTraceChecker = exprTraceChecker; + this.precRefiner = precRefiner; + this.pruneStrategy = pruneStrategy; + this.logger = logger; + this.emptyRefutation = emptyRefutation; + } + + public static SingleXtaTraceRefiner create(XtaTraceChecker zoneTraceChecker, + ExprTraceChecker exprTraceChecker, + PrecRefiner>, + XtaAction, XtaPrec>, Prod2Refutation> precRefiner, + PruneStrategy pruneStrategy, Logger logger, R emptyRefutation){ + return new SingleXtaTraceRefiner<>(zoneTraceChecker, exprTraceChecker, precRefiner, pruneStrategy, logger, emptyRefutation); + } + @Override + public RefinerResult>, XtaAction, XtaPrec>> refine(ARG>, XtaAction> arg, XtaPrec> prec) { + checkNotNull(arg); + checkNotNull(prec); + assert !arg.isSafe() : "ARG must be unsafe"; + + Optional>, XtaAction>> optionalNewCex = arg.getCexs().filter(cex -> ArgCexCheckHandler.instance.checkIfCounterexampleNew(cex)).findFirst(); + final ArgTrace>, XtaAction> cexToConcretize = optionalNewCex.get(); + + List zoneStates = cexToConcretize.nodes().stream().map(ArgNode::getState).map(XtaState::getState).map(Prod2State::getState2).collect(Collectors.toList()); + List actions = cexToConcretize.edges().stream().map(ArgEdge::getAction).toList(); + List exprStates = cexToConcretize.nodes().stream().map(ArgNode::getState).map(XtaState::getState).map(Prod2State::getState1).collect(Collectors.toList()); + //elvesztődnek az xta state infok, a exprtrace nél amikor megadom a configba át kell adni az init valuation okat + final Trace zoneTrace = Trace.of(zoneStates, actions); + final Trace exprTrace = Trace.of(exprStates, actions); + + + final ExprTraceStatus cexZoneStatus = zoneTraceChecker.check(zoneTrace); + + final ExprTraceStatus cexExprStatus = exprTraceChecker.check(exprTrace); + + final Trace>, XtaAction> traceToConcretize = cexToConcretize.toTrace(); + logger.write(Logger.Level.INFO, "| | Trace length: %d%n", traceToConcretize.length()); + logger.write(Logger.Level.DETAIL, "| | Trace: %s%n", traceToConcretize); + + logger.write(Logger.Level.SUBSTEP, "| | Checking trace..."); + + //final ExprTraceStatus cexStatus = exprTraceChecker.check(traceToConcretize); + logger.write(Logger.Level.SUBSTEP, "done, result: %s%n", cexZoneStatus); + logger.write(Logger.Level.SUBSTEP, "done, result: %s%n", cexExprStatus); + + assert cexZoneStatus.isFeasible() || cexZoneStatus.isInfeasible() : "Unknown CEX status"; + assert cexExprStatus.isFeasible() || cexExprStatus.isInfeasible() : "Unknown CEX status"; + + if (cexZoneStatus.isFeasible() && cexExprStatus.isFeasible()) { // if any of traces are feasible than it is unsafe + return RefinerResult.unsafe(traceToConcretize); + } else { + final ZoneRefutation zoneRefutation =cexZoneStatus.isInfeasible() ? cexZoneStatus.asInfeasible().getRefutation() : ZoneRefutation.emptyRefutation(); + final R exprRefutation = cexExprStatus.isInfeasible() ? cexExprStatus.asInfeasible().getRefutation() : emptyRefutation; + logger.write(Logger.Level.DETAIL, "| | | Refutation: %s%n", zoneRefutation); + logger.write(Logger.Level.DETAIL, "| | | Refutation: %s%n", exprRefutation); + + Prod2Refutation prod2Refutation = new Prod2Refutation(exprRefutation, zoneRefutation); + + final XtaPrec> refinedPrec = precRefiner.refine(prec, traceToConcretize, prod2Refutation); + final int pruneIndex = prod2Refutation.getPruneIndex(); + assert 0 <= pruneIndex : "Pruning index must be non-negative"; + assert pruneIndex <= cexToConcretize.length() : "Pruning index larger than cex length"; + + ArgCexCheckHandler.instance.addCounterexample(cexToConcretize); + + switch (pruneStrategy) { + case LAZY: + logger.write(Logger.Level.SUBSTEP, "| | Pruning from index %d...", pruneIndex); + final ArgNode>, XtaAction> nodeToPrune = cexToConcretize.node(pruneIndex); + arg.prune(nodeToPrune); + + break; + case FULL: + logger.write(Logger.Level.SUBSTEP, "| | Pruning whole ARG", pruneIndex); + arg.pruneAll(); + break; + default: + throw new UnsupportedOperationException("Unsupported pruning strategy"); + } + logger.write(Logger.Level.SUBSTEP, "done%n"); + + return RefinerResult.spurious(refinedPrec); + } + } + +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaClockPredUtils.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaClockPredUtils.java new file mode 100644 index 0000000000..cd775a4032 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaClockPredUtils.java @@ -0,0 +1,296 @@ +/* + * Copyright 2017 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import com.google.common.collect.Lists; +import hu.bme.mit.theta.analysis.zone.ClockPredPrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.core.clock.op.ResetOp; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.xta.Guard; +import hu.bme.mit.theta.xta.Update; +import hu.bme.mit.theta.xta.XtaProcess.Edge; +import hu.bme.mit.theta.xta.XtaProcess.Loc; +import hu.bme.mit.theta.xta.XtaProcess.LocKind; +import hu.bme.mit.theta.xta.analysis.XtaAction; +import hu.bme.mit.theta.xta.analysis.XtaAction.BasicXtaAction; +import hu.bme.mit.theta.xta.analysis.XtaAction.BinaryXtaAction; +import hu.bme.mit.theta.xta.analysis.XtaAction.BroadcastXtaAction; + +import java.util.Collection; +import java.util.List; + +import static com.google.common.base.Preconditions.checkNotNull; +import static hu.bme.mit.theta.core.clock.constr.ClockConstrs.Eq; + +public final class XtaClockPredUtils { + + private XtaClockPredUtils() { + } + + public static ZoneState post(final ZoneState state, final XtaAction action, final ClockPredPrec prec) { + checkNotNull(state); + checkNotNull(action); + checkNotNull(prec); + + if (action.isBasic()) { + return postForBasicAction(state, action.asBasic(), prec); + } else if (action.isBinary()) { + return postForBinaryAction(state, action.asBinary(), prec); + } else if (action.isBroadcast()) { + return postForBroadcastAction(state, action.asBroadcast(), prec); + } else { + throw new AssertionError(); + } + } + + private static ZoneState postForBasicAction(final ZoneState state, final BasicXtaAction action, + final ClockPredPrec prec) { + final ZoneState.Builder succStateBuilder = state.project(prec.getVars()); + + final List sourceLocs = action.getSourceLocs(); + final Edge edge = action.getEdge(); + final List targetLocs = action.getTargetLocs(); + + applyInvariants(succStateBuilder, sourceLocs); + applyGuards(succStateBuilder, edge); + applyUpdates(succStateBuilder, edge); + applyInvariants(succStateBuilder, targetLocs); + if (shouldApplyDelay(action.getTargetLocs())) { + applyDelay(succStateBuilder); + } + + final ZoneState succState = succStateBuilder.build(); + return succState; + } + + private static ZoneState postForBinaryAction(final ZoneState state, final BinaryXtaAction action, + final ClockPredPrec prec) { + final ZoneState.Builder succStateBuilder = state.project(prec.getVars()); + + final List sourceLocs = action.getSourceLocs(); + final Edge emittingEdge = action.getEmitEdge(); + final Edge receivingEdge = action.getRecvEdge(); + final List targetLocs = action.getTargetLocs(); + + applyInvariants(succStateBuilder, sourceLocs); + applyGuards(succStateBuilder, emittingEdge); + applyGuards(succStateBuilder, receivingEdge); + applyUpdates(succStateBuilder, emittingEdge); + applyUpdates(succStateBuilder, receivingEdge); + applyInvariants(succStateBuilder, targetLocs); + + if (shouldApplyDelay(targetLocs)) { + applyDelay(succStateBuilder); + } + + final ZoneState succState = succStateBuilder.build(); + return succState; + } + + private static ZoneState postForBroadcastAction(final ZoneState state, final BroadcastXtaAction action, + final ClockPredPrec prec) { + final ZoneState.Builder succStateBuilder = state.project(prec.getVars()); + + final List sourceLocs = action.getSourceLocs(); + final Edge emitEdge = action.getEmitEdge(); + final List recvEdges = action.getRecvEdges(); + final List> nonRecvEdgeCols = action.getNonRecvEdges(); + final List targetLocs = action.getTargetLocs(); + + applyInvariants(succStateBuilder, sourceLocs); + applyGuards(succStateBuilder, emitEdge); + + if (recvEdges.stream().anyMatch(XtaClockPredUtils::hasClockGuards)) { + throw new UnsupportedOperationException( + "Clock guards on edges with broadcast synchronization labels are not supported."); + } + + if (nonRecvEdgeCols.stream().anyMatch(c -> c.stream().anyMatch(XtaClockPredUtils::hasClockGuards))) { + throw new UnsupportedOperationException( + "Clock guards on edges with broadcast synchronization labels are not supported."); + } + + applyUpdates(succStateBuilder, emitEdge); + recvEdges.stream().forEachOrdered(recvEdge -> applyUpdates(succStateBuilder, recvEdge)); + applyInvariants(succStateBuilder, targetLocs); + + if (shouldApplyDelay(targetLocs)) { + applyDelay(succStateBuilder); + } + + final ZoneState succState = succStateBuilder.build(); + return succState; + } + + private static boolean hasClockGuards(Edge edge) { + return edge.getGuards().stream().anyMatch(Guard::isClockGuard); + } + + //// + + public static ZoneState pre(final ZoneState state, final XtaAction action, final ClockPredPrec prec) { + checkNotNull(state); + checkNotNull(action); + checkNotNull(prec); + + if (action.isBasic()) { + return preForBasicAction(state, action.asBasic(), prec); + } else if (action.isBinary()) { + return preForBinaryAction(state, action.asBinary(), prec); + } else if (action.isBroadcast()) { + return preForBroadcastAction(state, action.asBroadcast(), prec); + } else { + throw new AssertionError(); + } + } + + private static ZoneState preForBasicAction(final ZoneState state, final BasicXtaAction action, + final ClockPredPrec prec) { + final ZoneState.Builder preStateBuilder = state.project(prec.getVars()); + + final List sourceLocs = action.getSourceLocs(); + final Edge edge = action.getEdge(); + final List targetLocs = action.getTargetLocs(); + + if (shouldApplyDelay(action.getTargetLocs())) { + applyInverseDelay(preStateBuilder); + } + applyInvariants(preStateBuilder, targetLocs); + applyInverseUpdates(preStateBuilder, edge); + applyGuards(preStateBuilder, edge); + applyInvariants(preStateBuilder, sourceLocs); + + final ZoneState preState = preStateBuilder.build(); + return preState; + } + + private static ZoneState preForBinaryAction(final ZoneState state, final BinaryXtaAction action, + final ClockPredPrec prec) { + final ZoneState.Builder preStateBuilder = state.project(prec.getVars()); + + final List sourceLocs = action.getSourceLocs(); + final Edge emitEdge = action.getEmitEdge(); + final Edge recvEdge = action.getRecvEdge(); + final List targetLocs = action.getTargetLocs(); + + if (shouldApplyDelay(action.getTargetLocs())) { + applyInverseDelay(preStateBuilder); + } + applyInvariants(preStateBuilder, targetLocs); + applyInverseUpdates(preStateBuilder, recvEdge); + applyInverseUpdates(preStateBuilder, emitEdge); + applyGuards(preStateBuilder, recvEdge); + applyGuards(preStateBuilder, emitEdge); + applyInvariants(preStateBuilder, sourceLocs); + + final ZoneState succState = preStateBuilder.build(); + return succState; + } + + private static ZoneState preForBroadcastAction(final ZoneState state, final BroadcastXtaAction action, + final ClockPredPrec prec) { + final ZoneState.Builder preStateBuilder = state.project(prec.getVars()); + + final List sourceLocs = action.getSourceLocs(); + final Edge emitEdge = action.getEmitEdge(); + final List reverseRecvEdges = Lists.reverse(action.getRecvEdges()); + final List> nonRecvEdgeCols = action.getNonRecvEdges(); + final List targetLocs = action.getTargetLocs(); + + if (shouldApplyDelay(action.getTargetLocs())) { + applyInverseDelay(preStateBuilder); + } + applyInvariants(preStateBuilder, targetLocs); + reverseRecvEdges.stream().forEachOrdered(recvEdge -> applyInverseUpdates(preStateBuilder, recvEdge)); + applyInverseUpdates(preStateBuilder, emitEdge); + + if (nonRecvEdgeCols.stream().anyMatch(c -> c.stream().anyMatch(XtaClockPredUtils::hasClockGuards))) { + throw new UnsupportedOperationException( + "Clock guards on edges with broadcast synchronization labels are not supported."); + } + + if (reverseRecvEdges.stream().anyMatch(XtaClockPredUtils::hasClockGuards)) { + throw new UnsupportedOperationException( + "Clock guards on edges with broadcast synchronization labels are not supported."); + } + + applyGuards(preStateBuilder, emitEdge); + applyInvariants(preStateBuilder, sourceLocs); + + final ZoneState succState = preStateBuilder.build(); + return succState; + } + + //// + + private static boolean shouldApplyDelay(final List locs) { + return locs.stream().allMatch(l -> l.getKind() == LocKind.NORMAL); + } + + private static void applyDelay(final ZoneState.Builder builder) { + builder.nonnegative(); + builder.up(); + } + + private static void applyInverseDelay(final ZoneState.Builder builder) { + builder.down(); + builder.nonnegative(); + } + + private static void applyInvariants(final ZoneState.Builder builder, final Collection locs) { + for (final Loc target : locs) { + for (final Guard invar : target.getInvars()) { + if (invar.isClockGuard()) { + builder.and(invar.asClockGuard().getClockConstr()); + } + } + } + } + + private static void applyUpdates(final ZoneState.Builder builder, final Edge edge) { + for (final Update update : edge.getUpdates()) { + if (update.isClockUpdate()) { + final ResetOp op = (ResetOp) update.asClockUpdate().getClockOp(); + final VarDecl varDecl = op.getVar(); + final int value = op.getValue(); + builder.reset(varDecl, value); + } + } + } + + private static void applyInverseUpdates(final ZoneState.Builder builder, final Edge edge) { + for (final Update update : Lists.reverse(edge.getUpdates())) { + if (update.isClockUpdate()) { + final ResetOp op = (ResetOp) update.asClockUpdate().getClockOp(); + final VarDecl varDecl = op.getVar(); + final int value = op.getValue(); + builder.and(Eq(varDecl, value)); + builder.free(varDecl); + } + } + } + + private static void applyGuards(final ZoneState.Builder builder, final Edge edge) { + for (final Guard guard : edge.getGuards()) { + if (guard.isClockGuard()) { + builder.and(guard.asClockGuard().getClockConstr()); + } + } + } + +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java new file mode 100644 index 0000000000..43e5dc40a4 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java @@ -0,0 +1,84 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import hu.bme.mit.theta.analysis.Trace; +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.expr.refinement.ZoneRefutation; +import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.analysis.zone.ZonePrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; +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 hu.bme.mit.theta.core.utils.indexings.VarIndexing; +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; +import hu.bme.mit.theta.solver.ItpMarker; +import hu.bme.mit.theta.solver.ItpPattern; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.xta.analysis.XtaAction; +import hu.bme.mit.theta.xta.analysis.XtaState; +import hu.bme.mit.theta.xta.analysis.prec.XtaPrec; +import hu.bme.mit.theta.xta.analysis.zone.XtaZoneUtils; + +import java.util.ArrayList; +import java.util.List; + +import static com.google.common.base.Preconditions.checkNotNull; + +public class XtaTraceChecker { + + + private final ItpSolver solver; + private final Expr init; + + private final Expr target; + + private final ZonePrec clocks; + private XtaTraceChecker(final Expr init, final Expr target, final ItpSolver solver,ZonePrec clocks ) { + this.solver = solver; + this.init = init; + this.target = target; + this.clocks = clocks; + } + + public static XtaTraceChecker create(final Expr init, final Expr target, final ItpSolver solver, ZonePrec clocks) { + return new XtaTraceChecker(init, target, solver, clocks); + } + /* + interpoláns az utolsó zonestate dbm-e és a a konkrét között amit itt számolok ki + */ + public ExprTraceStatus check(Trace trace) { + final int stateCount = trace.getStates().size(); + final int actionCount = trace.getActions().size(); + final List concreteZoneStates = new ArrayList(stateCount); + final List abstractPreZoneStates = new ArrayList<>(stateCount); + + abstractPreZoneStates.add( trace.getState(stateCount-1)); + concreteZoneStates.add(trace.getState(0)); + + for(int i = 1; i < stateCount; i++){ + concreteZoneStates.add(XtaZoneUtils.post(trace.getState(i), trace.getAction(i-1), clocks)); + abstractPreZoneStates.add(ZoneState.intersection(XtaZoneUtils.pre( abstractPreZoneStates.get(i-1), trace.getAction(actionCount-i), clocks), + trace.getState(stateCount-1-i))); + } + //szerintem elég lenne az elsőt megnézni ahol a metszet bottom + int maxindex = 0; + boolean concretizable = true; + for (int i = stateCount-1; i >=0; i--){ + if(ZoneState.intersection(concreteZoneStates.get(i), abstractPreZoneStates.get(stateCount - 1 - i)).isBottom()){ + maxindex = i; concretizable = false; break; + } + } + if(concretizable){ + return ExprTraceStatus.feasible(null); + } + ZoneState interpolant = ZoneState.interpolant(concreteZoneStates.get(maxindex), abstractPreZoneStates.get(stateCount - 1 - maxindex)); + return ExprTraceStatus.infeasible(ZoneRefutation.binary(maxindex, interpolant, clocks.getVars().stream().toList() ,stateCount)); + } + + + +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/combinedlazycegar/CombinedLazyCegarXtaCheckerConfigFactory.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/combinedlazycegar/CombinedLazyCegarXtaCheckerConfigFactory.java deleted file mode 100644 index b192b554fd..0000000000 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/combinedlazycegar/CombinedLazyCegarXtaCheckerConfigFactory.java +++ /dev/null @@ -1,206 +0,0 @@ -package hu.bme.mit.theta.xta.analysis.combinedlazycegar; - -import hu.bme.mit.theta.analysis.*; -import hu.bme.mit.theta.analysis.algorithm.SearchStrategy; -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; -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.refinement.*; -import hu.bme.mit.theta.analysis.prod2.Prod2Analysis; -import hu.bme.mit.theta.analysis.prod2.Prod2Prec; -import hu.bme.mit.theta.analysis.prod2.Prod2State; -import hu.bme.mit.theta.analysis.zone.*; -import hu.bme.mit.theta.common.Tuple3; -import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.common.logging.NullLogger; -import hu.bme.mit.theta.core.utils.Lens; -import hu.bme.mit.theta.solver.SolverFactory; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; -import hu.bme.mit.theta.xta.XtaSystem; -import hu.bme.mit.theta.xta.analysis.*; -import hu.bme.mit.theta.xta.analysis.lazy.ClockStrategy; -import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaLensUtils; -import hu.bme.mit.theta.xta.analysis.zone.XtaZoneAnalysis; -import hu.bme.mit.theta.xta.analysis.zone.XtaZoneInvTransFunc; -import hu.bme.mit.theta.xta.analysis.zone.XtaZoneTransFunc; - -import java.util.function.Function; - -import static com.google.common.base.Preconditions.checkNotNull; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; -import static hu.bme.mit.theta.xta.analysis.combinedlazycegar.CombinedLazyCegarXtaUtils.forceCast; -import static hu.bme.mit.theta.xta.analysis.lazy.LazyXtaLensUtils.createConcrProd2Lens; - -public class CombinedLazyCegarXtaCheckerConfigFactory { - private final XtaSystem system; - private final Logger logger; - private final SolverFactory solverFactory; - - private CombinedLazyCegarXtaCheckerConfigFactory(final XtaSystem system, final Logger logger, final SolverFactory solverFactory) { - this.system = system; - this.logger = logger; - this.solverFactory = solverFactory; - } - - private CombinedLazyCegarXtaCheckerConfigFactory(final XtaSystem system) { - this(system, NullLogger.getInstance(), Z3SolverFactory.getInstance()); - } - - public static CombinedLazyCegarXtaCheckerConfigFactory create(final XtaSystem system, final Logger logger, final SolverFactory solverFactory) { - return new CombinedLazyCegarXtaCheckerConfigFactory(system, logger, solverFactory); - } - - public static CombinedLazyCegarXtaCheckerConfigFactory create(final XtaSystem system) { - return new CombinedLazyCegarXtaCheckerConfigFactory(system); - } - - public CombinedLazyCegarXtaCheckerConfig build() { - final var lazyStrategy = createLazyStrategy(ClockStrategy.BWITP); - - final var lazyAnalysis = createLazyAnalysis( - solverFactory, - lazyStrategy.getPartialOrd(), - lazyStrategy.getInitAbstractor() - ); - - final var prec = createConcrPrec(); - - final var cegarChecker = CegarChecker.create( - new LazyAbstractor<>( - forceCast(XtaLts.create(system)), - SearchStrategy.BFS, - lazyStrategy, - lazyAnalysis, - XtaState::isError, - createConcrProd2Lens() - ), - SingleExprTraceRefiner.create( - new CombinedLazyCegarExprTraceChecker<>( - ExprTraceSeqItpChecker.create(True(), True(), solverFactory.createItpSolver()), - createConcrProd2Lens(), - system), - new CombinedLazyCegarXtaPrecRefiner<>(new ItpRefToExplPrec()), - PruneStrategy.FULL, - logger - ), - logger - ); - - return new CombinedLazyCegarXtaCheckerConfig<>(cegarChecker, prec); - } - - private LazyAnalysis>, XtaState>, XtaAction, Prod2Prec> - createLazyAnalysis(final SolverFactory solverFactory, - final PartialOrd> abstrPartialOrd, - final InitAbstractor, Prod2State> initAbstractor) { - final Prod2Analysis - prod2ConcrAnalysis = createConcrAnalysis(solverFactory); - final XtaAnalysis, Prod2Prec> - xtaConcrAnalysis = XtaAnalysis.create(system, prod2ConcrAnalysis); - - return LazyAnalysis.create( - XtaOrd.create(abstrPartialOrd), - xtaConcrAnalysis.getInitFunc(), - xtaConcrAnalysis.getTransFunc(), - XtaInitAbstractor.create(initAbstractor) - ); - } - - private Prod2Analysis createConcrAnalysis(final SolverFactory solverFactory) { - return Prod2Analysis.create( - createConcrDataAnalysis(solverFactory), - createConcrClockAnalysis() - ); - } - - private Analysis createConcrDataAnalysis(final SolverFactory solverFactory) { - return CombinedLazyCegarXtaAnalysis.create( - ExplAnalysis.create( - solverFactory.createSolver(), - system.getInitVal().toExpr() - ) - ); - } - - private Analysis createConcrClockAnalysis() { - return XtaZoneAnalysis.getInstance(); - } - - private LazyStrategy, Prod2State, LazyState>, XtaState>>, XtaAction> - createLazyStrategy(final ClockStrategy clockStrategy) { - final LazyStrategy>, XtaState>>, XtaAction> - dataLazyStrategy = forceCast(createDataStrategy2()); - - final LazyStrategy>, XtaState>>, XtaAction> - clockLazyStrategy = forceCast(createClockStrategy(clockStrategy)); - - final Function>, XtaState>>, ?> projection = s -> Tuple3.of( - s.getConcrState().getLocs(), - dataLazyStrategy.getProjection().apply(s), - clockLazyStrategy.getProjection().apply(s) - ); - - final Lens>, XtaState>>, Prod2State> - lens = createConcrProd2Lens(); - return new Prod2LazyStrategy<>(lens, dataLazyStrategy, clockLazyStrategy, projection); - } - - private LazyStrategy>, XtaState>>, XtaAction> createDataStrategy2() { - return new BasicLazyStrategy<>( - createDataLens(), - createDataConcretizer() - ); - } - - private Lens>, XtaState>>, ExplState> createDataLens() { - return LazyXtaLensUtils.createConcrDataLens(); - } - - private Concretizer createDataConcretizer() { - return BasicConcretizer.create(ExplOrd.getInstance()); - } - - private LazyStrategy>, XtaState>>, XtaAction> createClockStrategy(final ClockStrategy clockStrategy) { - return switch (clockStrategy) { - case BWITP, FWITP -> createLazyZoneStrategy(clockStrategy); - case LU -> throw new AssertionError(); - }; - } - - private LazyStrategy>, XtaState>>, XtaAction> - createLazyZoneStrategy(final ClockStrategy clockStrategy) { - - final Lens>, XtaState>>, LazyState> - lens = LazyXtaLensUtils.createLazyClockLens(); - final Lattice lattice = ZoneLattice.getInstance(); - final Interpolator interpolator = ZoneInterpolator.getInstance(); - final PartialOrd partialOrd = ZoneOrd.getInstance(); - final Concretizer concretizer = BasicConcretizer.create(partialOrd); - final InvTransFunc zoneInvTransFunc = XtaZoneInvTransFunc.getInstance(); - final ZonePrec prec = ZonePrec.of(system.getClockVars()); - - switch (clockStrategy){ - case BWITP: - return new BwItpStrategy<>(lens, lattice, interpolator, concretizer, zoneInvTransFunc, prec); - case FWITP: - final TransFunc zoneTransFunc = XtaZoneTransFunc.getInstance(); - return new FwItpStrategy<>(lens, lattice, interpolator, concretizer, zoneInvTransFunc, prec, zoneTransFunc, prec); - default: - throw new AssertionError(); - } - } - - private Prod2Prec createConcrPrec() { - return Prod2Prec.of(createConcrDataPrec(), createConcrZonePrec()); - } - - private ExplPrec createConcrDataPrec() { - return ExplPrec.empty(); - } - - private ZonePrec createConcrZonePrec() { - return ZonePrec.of(system.getClockVars()); - } - -} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfig.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfig.java index 93166242a4..d1f8ea9f02 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfig.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfig.java @@ -6,7 +6,7 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -public final class XtaConfig { +public final class XtaConfig{ private final SafetyChecker checker; private final P initPrec; private XtaConfig(final SafetyChecker checker, final P initPrec) { diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java new file mode 100644 index 0000000000..a58a2590be --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java @@ -0,0 +1,485 @@ +package hu.bme.mit.theta.xta.analysis.config; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.State; +import hu.bme.mit.theta.analysis.algorithm.ArgBuilder; +import hu.bme.mit.theta.analysis.algorithm.ArgNodeComparators; +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; +import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor; +import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor; +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.cegar.abstractor.StopCriterions; +import hu.bme.mit.theta.analysis.expl.*; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.expr.refinement.*; +import hu.bme.mit.theta.analysis.pred.*; +import hu.bme.mit.theta.analysis.prod2.Prod2Analysis; +import hu.bme.mit.theta.analysis.prod2.Prod2Prec; +import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist; +import hu.bme.mit.theta.analysis.zone.ClockPredPrec; +import hu.bme.mit.theta.analysis.zone.ZonePrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.common.logging.NullLogger; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.xta.XtaProcess; +import hu.bme.mit.theta.xta.XtaSystem; +import hu.bme.mit.theta.xta.analysis.*; +import hu.bme.mit.theta.solver.*; +import hu.bme.mit.theta.xta.analysis.ClockPred.*; +import hu.bme.mit.theta.xta.analysis.prec.*; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; + +public class XtaConfigBuilder_ClockPred { + public enum Domain { + EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT + } + + public enum Refinement { + FW_BIN_ITP, BW_BIN_ITP, SEQ_ITP, MULTI_SEQ, UNSAT_CORE, UCB, + NWT_WP, NWT_SP, NWT_WP_LV, NWT_SP_LV, NWT_IT_WP, NWT_IT_SP, NWT_IT_WP_LV, NWT_IT_SP_LV + } + public enum Search { + BFS(ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())), + + DFS(ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.dfs())); + + public final ArgNodeComparators.ArgNodeComparator comparator; + + private Search(final ArgNodeComparators.ArgNodeComparator comparator) { + this.comparator = comparator; + } + + } + + + + public enum PredSplit { + WHOLE(ExprSplitters.whole()), + + CONJUNCTS(ExprSplitters.conjuncts()), + + ATOMS(ExprSplitters.atoms()); + + public final ExprSplitters.ExprSplitter splitter; + + private PredSplit(final ExprSplitters.ExprSplitter splitter) { + this.splitter = splitter; + } + } + //TODO more InitPrec needed + public enum InitPrec { + EMPTY, ALLVARS, ALLASSUMES + } + public enum PrecGranularity{ + GLOBAL { + + public

XtaPrec

createPrec(final P innerPrec) { + return GlobalXtaPrec.create(innerPrec); + } + + + public PrecRefiner>, XtaAction, XtaPrec>, Prod2Refutation> createRefiner( + final RefutationToPrec, Prod2Refutation> refToPrec) { + return GlobalXtaPrecRefiner.create(refToPrec); + } + }, + LOCAL { + + public

XtaPrec

createPrec(final P innerPrec) { + return LocalXtaPrec.create(innerPrec); + } + + + public PrecRefiner>, XtaAction, XtaPrec>, Prod2Refutation> createRefiner( + final RefutationToPrec, Prod2Refutation> refToPrec) { + return LocalXtaPrecRefiner.create(refToPrec); + } + }; + public abstract

XtaPrec

createPrec(final P innerPrec); + public abstract PrecRefiner>, XtaAction, XtaPrec>, Prod2Refutation> createRefiner( + final RefutationToPrec, Prod2Refutation> refToPrec); + + + } + + + private Logger logger = NullLogger.getInstance(); + private final SolverFactory abstractionSolverFactory; + private final SolverFactory refinementSolverFactory; + private final Domain domain; + private final Refinement refinement; + private Search search = Search.BFS; + private PredSplit predSplit = PredSplit.WHOLE; + private PrecGranularity precGranularity = PrecGranularity.GLOBAL; + private int maxEnum = 0; + private InitPrec initPrec = InitPrec.EMPTY; + private PruneStrategy pruneStrategy = PruneStrategy.LAZY; + + + public XtaConfigBuilder_ClockPred(final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { + this.domain = domain; + this.refinement = refinement; + this.abstractionSolverFactory = solverFactory; + this.refinementSolverFactory = solverFactory; + } + public XtaConfigBuilder_ClockPred(final Domain domain, final Refinement refinement, final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) { + this.domain = domain; + this.refinement = refinement; + this.abstractionSolverFactory = abstractionSolverFactory; + this.refinementSolverFactory = refinementSolverFactory; + } + public XtaConfigBuilder_ClockPred logger(final Logger logger) { + this.logger = logger; + return this; + } + public XtaConfigBuilder_ClockPred search(final Search search) { + this.search = search; + return this; + } + public XtaConfigBuilder_ClockPred predSplit(final PredSplit predSplit) { + this.predSplit = predSplit; + return this; + } + public XtaConfigBuilder_ClockPred precGranularity(final PrecGranularity precGranularity) { + this.precGranularity = precGranularity; + + return this; + } + public XtaConfigBuilder_ClockPred maxEnum(final int maxEnum) { + this.maxEnum = maxEnum; + return this; + } + public XtaConfigBuilder_ClockPred initPrec(final InitPrec initPrec) { + this.initPrec = initPrec; + return this; + } + public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrategy) { + this.pruneStrategy = pruneStrategy; + return this; + } + public XtaConfig build(final XtaSystem xta) { + final XtaLts lts = XtaLts.create(xta); + //final Expr negProp = xta + final Expr initval = xta.getInitVal().toExpr(); + + if(domain == Domain.EXPL){ + final Analysis, XtaAction, Prod2Prec> prod2Analysis = Prod2Analysis.create( + ExplStmtAnalysis.create(abstractionSolverFactory.createSolver(), xta.getInitVal().toExpr(), maxEnum), + ClockPredAnalysis.getInstance() + ); + final Analysis>, XtaAction, XtaPrec>> analysis = XtaAnalysis.create(xta,prod2Analysis); + + //TODO analysis + final ArgBuilder>,XtaAction, XtaPrec>> argbuilder = ArgBuilder.create(lts, analysis, s -> s.getLocs().stream().anyMatch(l -> l.getKind().equals(XtaProcess.LocKind.ERROR)), true); + final Abstractor>, XtaAction, XtaPrec>> abstractor = BasicAbstractor.builder(argbuilder) + .waitlist(PriorityWaitlist.create(search.comparator)) + .stopCriterion(refinement == Refinement.MULTI_SEQ ? StopCriterions.fullExploration() : StopCriterions.firstCex()) + .logger(logger).build() + ; + Refiner>, XtaAction, XtaPrec>> refiner; + + final RefutationToPrec, Prod2Refutation> reftoprec = new Prod2RefToProd2ExplClockPredPrec(); + //it should be generic but for testing I use only ItpRefutation + ItpRefutation emptyRefutation = ItpRefutation.emptyRefutation(); + switch (refinement) { + case FW_BIN_ITP: + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), + precGranularity.createRefiner(reftoprec), + pruneStrategy, logger, emptyRefutation + ); + break; + case BW_BIN_ITP: + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), + precGranularity.createRefiner(reftoprec), + pruneStrategy, logger, emptyRefutation + ); + break; + case SEQ_ITP: + refiner =SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), + precGranularity.createRefiner(reftoprec), + pruneStrategy, logger, emptyRefutation + ); + break; + case MULTI_SEQ: + refiner =SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), + precGranularity.createRefiner(reftoprec), + pruneStrategy, logger, emptyRefutation + ); + break; + //TODO + /* + case UNSAT_CORE: + refiner = SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(True(), True(), refinementSolverFactory.createUCSolver()), + precGranularity.createRefiner(new VarsRefToExplPrec()), pruneStrategy, logger); + break;*/ + case UCB: + refiner =SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), + precGranularity.createRefiner(reftoprec), + pruneStrategy, logger, emptyRefutation + ); + break; + case NWT_SP: + refiner =SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withoutLV(), + precGranularity.createRefiner(reftoprec), + pruneStrategy, logger, emptyRefutation + ); + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withoutLV(), + precGranularity.createRefiner(reftoprec ), + pruneStrategy, + logger, emptyRefutation + ); + break; + case NWT_WP: + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withoutLV(), + precGranularity.createRefiner(reftoprec ), + pruneStrategy, + logger, emptyRefutation + ); + break; + case NWT_SP_LV: + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withLV(), + precGranularity.createRefiner(reftoprec ), + pruneStrategy, + logger, emptyRefutation + ); + break; + case NWT_WP_LV: + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withLV(), + precGranularity.createRefiner(reftoprec ), + pruneStrategy, + logger, emptyRefutation + ); + break; + case NWT_IT_SP: + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withoutLV(), + precGranularity.createRefiner(reftoprec ), + pruneStrategy, + logger, emptyRefutation + ); + break; + case NWT_IT_WP: + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withoutLV(), + precGranularity.createRefiner(reftoprec ), + pruneStrategy, + logger, emptyRefutation + ); + break; + case NWT_IT_SP_LV: + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withLV(), + precGranularity.createRefiner( reftoprec ), + pruneStrategy, + logger, emptyRefutation + ); + break; + case NWT_IT_WP_LV: + refiner = SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withLV(), + precGranularity.createRefiner(reftoprec ), + pruneStrategy, + logger, emptyRefutation + ); + break; + default: + throw new UnsupportedOperationException( + domain + " domain does not support " + refinement + " refinement."); + } + + final SafetyChecker>, XtaAction, XtaPrec>> checker = CegarChecker.create( + abstractor,refiner, logger); + XtaPrec> prec; + + switch (initPrec) { + case EMPTY: + prec = precGranularity.createPrec(XtaInitClockPredPrec.createEmptyProd2ExplZone(xta)); + break; + case ALLASSUMES: + switch (precGranularity) { + case LOCAL: + prec = XtaInitClockPredPrec.collectLocalProd2ExplZone(xta); + break; + case GLOBAL: + //It returns the same as empty prec + prec = XtaInitClockPredPrec.collectGlobalProd2ExplZone(xta); + break; + default: + throw new UnsupportedOperationException(precGranularity + + " precision granularity is not supported with " + domain + " domain"); + } + break; + default: + throw new UnsupportedOperationException(initPrec + " initial precision is not supported with " + + domain + " domain"); + } + return XtaConfig.create(checker, prec); + + } + + + + if(domain == Domain.PRED_BOOL || domain == Domain.PRED_CART || domain == Domain.PRED_SPLIT){ + final Solver analysisSolver = abstractionSolverFactory.createSolver(); + PredAbstractors.PredAbstractor predAbstractor; + switch (domain) { + case PRED_BOOL: + predAbstractor = PredAbstractors.booleanAbstractor(analysisSolver); + break; + case PRED_SPLIT: + predAbstractor = PredAbstractors.booleanSplitAbstractor(analysisSolver); + break; + case PRED_CART: + predAbstractor = PredAbstractors.cartesianAbstractor(analysisSolver); + break; + default: + throw new UnsupportedOperationException(domain + " domain is not supported."); + } + final Analysis, XtaAction, Prod2Prec> prod2Analysis = Prod2Analysis.create( + PredAnalysis.create(analysisSolver, predAbstractor, xta.getInitVal().toExpr()), + ClockPredAnalysis.getInstance() + ); + final Analysis>, XtaAction, XtaPrec>> analysis = XtaAnalysis.create(xta,prod2Analysis); + + //TODO analysis + final ArgBuilder>,XtaAction, XtaPrec>> argbuilder = ArgBuilder.create(lts, analysis, s -> s.getLocs().stream().anyMatch(l -> l.getKind().equals(XtaProcess.LocKind.ERROR)), true); + final Abstractor>, XtaAction, XtaPrec>> abstractor = BasicAbstractor.builder(argbuilder) + .waitlist(PriorityWaitlist.create(search.comparator)) + .stopCriterion(refinement == Refinement.MULTI_SEQ ? StopCriterions.fullExploration() : StopCriterions.firstCex()) + .logger(logger).build() + ; + + ExprTraceChecker exprTraceChecker; + switch (refinement) { + case FW_BIN_ITP: + exprTraceChecker = ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()); + break; + case BW_BIN_ITP: + exprTraceChecker = ExprTraceBwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()); + break; + case SEQ_ITP: + exprTraceChecker = ExprTraceSeqItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()); + break; + case MULTI_SEQ: + exprTraceChecker = ExprTraceSeqItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()); + break; + case UCB: + exprTraceChecker = ExprTraceUCBChecker.create(initval, True(), refinementSolverFactory.createUCSolver()); + break; + case NWT_SP: + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withoutLV(); + break; + case NWT_WP: + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withoutLV(); + break; + case NWT_SP_LV: + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withLV(); + break; + case NWT_WP_LV: + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withLV(); + break; + case NWT_IT_SP: + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withoutLV(); + break; + case NWT_IT_WP: + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withoutLV(); + break; + case NWT_IT_SP_LV: + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withLV(); + break; + case NWT_IT_WP_LV: + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withLV(); + break; + default: + throw new UnsupportedOperationException( + domain + " domain does not support " + refinement + " refinement."); + } + final RefutationToPrec, Prod2Refutation> reftoprec = new Prod2RefToProd2PredClockPredPrec(predSplit.splitter); + + //final RefutationToPrec, Prod2Refutation> reftoprec = ItpRefToProd2PredClockPredPrec.create(predSplit.splitter, ClockPredPrec.of(xta.getClockVars())); + //it should be generic but for testing I use only ItpRefutation + ItpRefutation emptyRefutation = ItpRefutation.emptyRefutation(); + Refiner>, XtaAction, XtaPrec>> refiner = + SingleXtaTraceRefiner.create( + XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + exprTraceChecker, + precGranularity.createRefiner(reftoprec), + pruneStrategy, + logger, emptyRefutation + ); + + PrecRefiner>, XtaAction, Prod2Prec, Prod2Refutation> precRefiner + = JoiningPrecRefiner.create(reftoprec); + /*if (refinement == Refinement.MULTI_SEQ) { + refiner = MultiExprTraceRefiner.create(exprTraceChecker, precGranularity.createRefiner(reftoprec), pruneStrategy, logger); + } else { + refiner = SingleExprTraceRefiner.create(exprTraceChecker, + precGranularity.createRefiner(reftoprec), pruneStrategy, logger); + }*/ + + final SafetyChecker>, XtaAction, XtaPrec>> checker = CegarChecker.create( + abstractor,refiner, logger); + + XtaPrec> prec; + switch (initPrec) { + case EMPTY: + prec = precGranularity.createPrec(XtaInitClockPredPrec.createEmptyProd2PredZone(xta)); + break; + case ALLASSUMES: + switch (precGranularity) { + case LOCAL: + prec = XtaInitClockPredPrec.collectLocalProd2PredZone(xta); + break; + case GLOBAL: + //It returns the same as empty prec + prec = XtaInitClockPredPrec.collectGlobalProd2PredZone(xta); + break; + default: + throw new UnsupportedOperationException(precGranularity + + " precision granularity is not supported with " + domain + " domain"); + } + break; + default: + throw new UnsupportedOperationException(initPrec + " initial precision is not supported with " + + domain + " domain"); + } + return XtaConfig.create(checker, prec); + } + //TODO : + // Only works with Prod2Prec + + return null; + } + +} \ No newline at end of file diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_Zone.java similarity index 95% rename from subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder.java rename to subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_Zone.java index 9b895b85af..5774865330 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_Zone.java @@ -33,7 +33,7 @@ import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; -public class XtaConfigBuilder { +public class XtaConfigBuilder_Zone { public enum Domain { EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT } @@ -95,7 +95,7 @@ public

XtaPrec

createPrec(final P innerPrec) { public PrecRefiner, A, XtaPrec

, R> createRefiner( - final RefutationToPrec refToPrec) { + final RefutationToPrec refToPrec) { return LocalXtaPrecRefiner.create(refToPrec); } }; @@ -120,44 +120,44 @@ public abstract createEmptyProd2PredZone(XtaSystem xta){ + return Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(xta.getClockVars())); + } + + public static Prod2Prec createEmptyZoneProd2PredZone(XtaSystem xta) { + return Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(Collections.emptySet())); + } + public static LocalXtaPrec> collectLocalProd2PredZone(XtaSystem xta) { + Map> mapping = Containers.createMap(); + for(XtaProcess proc: xta.getProcesses()){ + for (XtaProcess.Loc l : proc.getActiveClockMap().keySet()){ + mapping.put(l, Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(proc.getActiveClockMap().get(l)))); + } + } + return LocalXtaPrec.create(mapping, Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(xta.getClockVars()))); + } + + public static GlobalXtaPrec> collectGlobalProd2PredZone(XtaSystem xta) { + return GlobalXtaPrec.create(Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(xta.getClockVars()))); + } + + public static Prod2Prec createEmptyProd2ExplZone(XtaSystem xta) { + return Prod2Prec.of(ExplPrec.empty(), ClockPredPrec.of(xta.getClockVars())); + } + + public static XtaPrec> collectLocalProd2ExplZone(XtaSystem xta) { + Map> mapping = Containers.createMap(); + for(XtaProcess proc: xta.getProcesses()){ + for (XtaProcess.Loc l : proc.getActiveClockMap().keySet()){ + mapping.put(l, Prod2Prec.of(ExplPrec.empty(), ClockPredPrec.of(proc.getActiveClockMap().get(l)))); + } + } + return LocalXtaPrec.create(mapping, Prod2Prec.of(ExplPrec.empty(), ClockPredPrec.of(xta.getClockVars()))); + } + + public static XtaPrec> collectGlobalProd2ExplZone(XtaSystem xta) { + return GlobalXtaPrec.create(Prod2Prec.of(ExplPrec.empty(), ClockPredPrec.of(xta.getClockVars()))); + } +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/prec/XtaInitPrec.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/prec/XtaInitPrec.java index d860a6ecd0..a4dc38621c 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/prec/XtaInitPrec.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/prec/XtaInitPrec.java @@ -4,18 +4,26 @@ import hu.bme.mit.theta.analysis.expl.ExplPrec; import hu.bme.mit.theta.analysis.pred.PredPrec; import hu.bme.mit.theta.analysis.prod2.Prod2Prec; +import hu.bme.mit.theta.analysis.zone.ClockPredPrec; +import hu.bme.mit.theta.analysis.zone.Pair; import hu.bme.mit.theta.analysis.zone.ZonePrec; import hu.bme.mit.theta.common.container.Containers; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.rattype.RatType; import hu.bme.mit.theta.xta.XtaProcess; import hu.bme.mit.theta.xta.XtaSystem; -import java.util.Map; +import java.util.*; +import java.util.stream.Collectors; public final class XtaInitPrec{ - public static Prod2Prec createEmptyProd2PredZone(XtaSystem xta){ + public static Prod2Prec createEmptyProd2PredZone(XtaSystem xta){ return Prod2Prec.of(PredPrec.of(), ZonePrec.of(xta.getClockVars())); } + public static Prod2Prec createEmptyZoneProd2PredZone(XtaSystem xta) { + return Prod2Prec.of(PredPrec.of(), ZonePrec.of(Collections.emptySet())); + } public static LocalXtaPrec> collectLocalProd2PredZone(XtaSystem xta) { Map> mapping = Containers.createMap(); for(XtaProcess proc: xta.getProcesses()){ @@ -26,11 +34,11 @@ public static LocalXtaPrec> collectLocalProd2PredZ return LocalXtaPrec.create(mapping, Prod2Prec.of(PredPrec.of(), ZonePrec.of(xta.getClockVars()))); } - public static GlobalXtaPrec> collectGlobalProd2PredZone(XtaSystem xta) { + public static GlobalXtaPrec> collectGlobalProd2PredZone(XtaSystem xta) { return GlobalXtaPrec.create(Prod2Prec.of(PredPrec.of(), ZonePrec.of(xta.getClockVars()))); } - public static Prod2Prec createEmptyProd2ExplZone(XtaSystem xta) { + public static Prod2Prec createEmptyProd2ExplZone(XtaSystem xta) { return Prod2Prec.of(ExplPrec.empty(), ZonePrec.of(xta.getClockVars())); } @@ -44,7 +52,15 @@ public static XtaPrec> collectLocalProd2ExplZone(X return LocalXtaPrec.create(mapping, Prod2Prec.of(ExplPrec.empty(), ZonePrec.of(xta.getClockVars()))); } - public static XtaPrec> collectGlobalProd2ExplZone(XtaSystem xta) { + public static XtaPrec> collectGlobalProd2ExplZone(XtaSystem xta) { return GlobalXtaPrec.create(Prod2Prec.of(ExplPrec.empty(), ZonePrec.of(xta.getClockVars()))); } + + /* public static XtaPrec> createTestPrec(XtaSystem xta) { + ArrayList> clocks = new ArrayList>(xta.getClockVars()); + Map, VarDecl>, Integer> map = Collections.emptyMap(); + Pair, VarDecl> pair = new Pair, VarDecl>(clocks.get(0), clocks.get(1)); + map.put(new Pair, VarDecl>(clocks.get(0), clocks.get(1)), (10 << 1) | 1); + return GlobalXtaPrec.create(Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(map, xta.getClockVars()))); + }*/ } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneAnalysis.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneAnalysis.java index 5446014a2f..c9985a83c0 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneAnalysis.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneAnalysis.java @@ -22,9 +22,10 @@ import hu.bme.mit.theta.analysis.zone.ZoneOrd; import hu.bme.mit.theta.analysis.zone.ZonePrec; import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.xta.analysis.ClockPred.ClockAnalysis; import hu.bme.mit.theta.xta.analysis.XtaAction; -public final class XtaZoneAnalysis implements Analysis { +public final class XtaZoneAnalysis implements Analysis { private static final XtaZoneAnalysis INSTANCE = new XtaZoneAnalysis(); diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneTransFunc.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneTransFunc.java index cff76433da..25dc44e9c3 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneTransFunc.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/zone/XtaZoneTransFunc.java @@ -38,6 +38,9 @@ static XtaZoneTransFunc getInstance() { @Override public Collection getSuccStates(final ZoneState state, final XtaAction action, final ZonePrec prec) { final ZoneState succState = XtaZoneUtils.post(state, action, prec); + //saját prec amiben óra párok és értékek vannak, ha a succStateben lévő dbm ben felül tudunk + //becsülni akkor felülbecslünk, ha nem akkor top + return ImmutableList.of(succState); } diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_ClockPred.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_ClockPred.java new file mode 100644 index 0000000000..a4048c0afc --- /dev/null +++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_ClockPred.java @@ -0,0 +1,65 @@ +package hu.bme.mit.theta.xta.analysis; + +import hu.bme.mit.theta.analysis.algorithm.SafetyResult; +import hu.bme.mit.theta.common.OsHelper; +import hu.bme.mit.theta.common.logging.ConsoleLogger; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.solver.SolverFactory; +import hu.bme.mit.theta.solver.SolverManager; +import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager; +import hu.bme.mit.theta.solver.z3.Z3SolverFactory; +import hu.bme.mit.theta.solver.z3.Z3SolverManager; +import hu.bme.mit.theta.xta.XtaSystem; +import hu.bme.mit.theta.xta.analysis.config.XtaConfig; +import hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder_ClockPred; +import hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder_Zone; +import hu.bme.mit.theta.xta.dsl.XtaDslManager; +import org.junit.Test; + +import java.io.FileInputStream; +import java.io.InputStream; +import java.io.SequenceInputStream; + +public class Test_ClockPred { + public XtaConfigBuilder_ClockPred.Domain domain; + + public XtaConfigBuilder_ClockPred.Refinement refinement; + + private Test_ClockPred instance; + + @Test + public void main(){ + instance = new Test_ClockPred(); + try{ + instance.check(); + }catch (Exception e){ + e.printStackTrace(); + } + } + + public void check() throws Exception{ + domain = XtaConfigBuilder_ClockPred.Domain.PRED_CART; + refinement = XtaConfigBuilder_ClockPred.Refinement.SEQ_ITP; + SolverManager.registerSolverManager(Z3SolverManager.create()); + if(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)) { + SolverManager.registerSolverManager(SmtLibSolverManager.create(SmtLibSolverManager.HOME, new ConsoleLogger(Logger.Level.DETAIL))); + } + + final SolverFactory solverFactory; + + solverFactory = SolverManager.resolveSolverFactory("Z3"); + + XtaSystem system; + try(InputStream inputStream = new SequenceInputStream(new FileInputStream("src/test/resources/model/ClockPredTest.xta"), new FileInputStream("src/test/resources/property/ClockPredTest.prop"))){ + system = XtaDslManager.createSystem(inputStream); + } + XtaConfigBuilder_ClockPred builder = new XtaConfigBuilder_ClockPred(domain, refinement, /*solverFactory*/ Z3SolverFactory.getInstance()); + builder.precGranularity(XtaConfigBuilder_ClockPred.PrecGranularity.GLOBAL); + builder.initPrec(XtaConfigBuilder_ClockPred.InitPrec.EMPTY); + builder.maxEnum(1); + + XtaConfig config = builder.build(system); + SafetyResult result = config.check(); + System.out.println("Safe?: " + result.isSafe()); + } +} diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_v1.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_v1.java index 210eaee3d3..8e3dc48955 100644 --- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_v1.java +++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_v1.java @@ -1,19 +1,5 @@ package hu.bme.mit.theta.xta.analysis; -import hu.bme.mit.theta.analysis.Action; -import hu.bme.mit.theta.analysis.Analysis; -import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.State; -import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -import hu.bme.mit.theta.analysis.expr.StmtAction; -import hu.bme.mit.theta.analysis.pred.PredAnalysis; -import hu.bme.mit.theta.analysis.pred.PredPrec; -import hu.bme.mit.theta.analysis.pred.PredState; -import hu.bme.mit.theta.analysis.prod2.Prod2Analysis; -import hu.bme.mit.theta.analysis.prod2.Prod2Prec; -import hu.bme.mit.theta.analysis.prod2.Prod2State; -import hu.bme.mit.theta.analysis.zone.ZonePrec; -import hu.bme.mit.theta.analysis.zone.ZoneState; import hu.bme.mit.theta.common.OsHelper; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; @@ -23,9 +9,7 @@ import hu.bme.mit.theta.solver.z3.Z3SolverFactory; import hu.bme.mit.theta.solver.z3.Z3SolverManager; import hu.bme.mit.theta.xta.XtaSystem; -import hu.bme.mit.theta.xta.analysis.config.XtaConfig; -import hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder; -import hu.bme.mit.theta.xta.analysis.prec.XtaPrec; +import hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder_Zone; import hu.bme.mit.theta.xta.dsl.XtaDslManager; import org.junit.Test; @@ -36,8 +20,8 @@ public class Test_v1 { public String solver; public String filepath; - public XtaConfigBuilder.Domain domain; - public XtaConfigBuilder.Refinement refinement; + public XtaConfigBuilder_Zone.Domain dataDomain; + public XtaConfigBuilder_Zone.Refinement refinement; private Test_v1 instance; @@ -53,8 +37,8 @@ public void main(){ } public void check() throws Exception { - domain = XtaConfigBuilder.Domain.EXPL; - refinement = XtaConfigBuilder.Refinement.SEQ_ITP; + dataDomain = XtaConfigBuilder_Zone.Domain.PRED_CART; + refinement = XtaConfigBuilder_Zone.Refinement.SEQ_ITP; SolverManager.registerSolverManager(Z3SolverManager.create()); if(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)) { SolverManager.registerSolverManager(SmtLibSolverManager.create(SmtLibSolverManager.HOME, new ConsoleLogger(Logger.Level.DETAIL))); @@ -65,17 +49,21 @@ public void check() throws Exception { solverFactory = SolverManager.resolveSolverFactory("Z3"); XtaSystem system; - try( InputStream inputStream = new SequenceInputStream(new FileInputStream("src/test/resources/model/mytest.xta"), new FileInputStream("src/test/resources/property/mytest.prop"))){ + try( InputStream inputStream = new SequenceInputStream(new FileInputStream("src/test/resources/model/ClockPredTest.xta"), new FileInputStream("src/test/resources/property/ClockPredTest.prop"))){ system = XtaDslManager.createSystem(inputStream); } + /*try( InputStream inputStream = new SequenceInputStream(new FileInputStream("src/test/resources/model/mytest.xta"), new FileInputStream("src/test/resources/property/mytest.prop"))){ + system = XtaDslManager.createSystem(inputStream); + }*/ - XtaConfigBuilder builder = new XtaConfigBuilder(domain, refinement, /*solverFactory*/ Z3SolverFactory.getInstance()); - builder.precGranularity(XtaConfigBuilder.PrecGranularity.GLOBAL); - builder.initPrec(XtaConfigBuilder.InitPrec.EMPTY); - XtaConfig config = + XtaConfigBuilder_Zone builder = new XtaConfigBuilder_Zone(dataDomain, refinement, /*solverFactory*/ Z3SolverFactory.getInstance()); + builder.precGranularity(XtaConfigBuilder_Zone.PrecGranularity.GLOBAL); + builder.initPrec(XtaConfigBuilder_Zone.InitPrec.EMPTY); + builder.maxEnum(1); + /*XtaConfig config = builder.build(system); SafetyResult result = config.check(); - System.out.println("Safe? : " + result.isSafe()); + System.out.println("Safe? : " + result.isSafe());*/ } } \ No newline at end of file diff --git a/subprojects/xta/xta-analysis/src/test/resources/model/ClockPredTest.xta b/subprojects/xta/xta-analysis/src/test/resources/model/ClockPredTest.xta new file mode 100644 index 0000000000..63e223791a --- /dev/null +++ b/subprojects/xta/xta-analysis/src/test/resources/model/ClockPredTest.xta @@ -0,0 +1,21 @@ +clock x; +clock y; + +int a = 0; +process P1(){ + + state + idle , + A {y <= 2}, + B; + + + init + idle; + + trans + idle -> A {guard x <= 5; assign y = 0;}, + A -> B {guard x >=7 ;assign a = 3;}; + +} +system P1; \ No newline at end of file diff --git a/subprojects/xta/xta-analysis/src/test/resources/model/mytest.xta b/subprojects/xta/xta-analysis/src/test/resources/model/mytest.xta index ae299fa0bd..e658f45d04 100644 --- a/subprojects/xta/xta-analysis/src/test/resources/model/mytest.xta +++ b/subprojects/xta/xta-analysis/src/test/resources/model/mytest.xta @@ -4,21 +4,24 @@ clock z; int a = 0; bool b = false; +broadcast chan ch; process P1(){ state idle , A { y < 5 }, B, - C ; + C , + c; - commit idle; + commit idle,c; init - A; + idle; trans - idle -> A {}, + idle -> A { guard x < 1; sync ch!;}, + c -> A {}, A -> A {guard x == 1; assign a = a + 1, x = 0, b = true;}, A -> B {guard a == 4 ;}, A -> C {guard a == 3;}; diff --git a/subprojects/xta/xta-analysis/src/test/resources/property/ClockPredTest.prop b/subprojects/xta/xta-analysis/src/test/resources/property/ClockPredTest.prop new file mode 100644 index 0000000000..74d4ac7740 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/test/resources/property/ClockPredTest.prop @@ -0,0 +1,3 @@ +prop{ + E<> P1_B +} \ No newline at end of file diff --git a/subprojects/xta/xta-analysis/src/test/resources/property/csma-2.prop b/subprojects/xta/xta-analysis/src/test/resources/property/csma-2.prop index da3ea8a300..e2c8e5bb5f 100644 --- a/subprojects/xta/xta-analysis/src/test/resources/property/csma-2.prop +++ b/subprojects/xta/xta-analysis/src/test/resources/property/csma-2.prop @@ -1,3 +1,3 @@ -prop{ - A[] (Station_0_transm && Station_1_transm && Station_0_x>2*SIGMA) +prop { +A[] not (Station_0_transm && Station_1_transm && Station_0_x>2*SIGMA) } \ No newline at end of file diff --git a/subprojects/xta/xta-cli/README.md b/subprojects/xta/xta-cli/README.md index a835f8cf23..549fb85e63 100644 --- a/subprojects/xta/xta-cli/README.md +++ b/subprojects/xta/xta-cli/README.md @@ -4,7 +4,7 @@ This project contains an executable tool (command line) for running analyses on ### Related projects -* [`xta`](../xta/README.md): Classes to represent XTAs and a domain specific language (DSL) to parse XTAs from a textual representation. +* [`xta`](../xta/README.md): Classes to represent XTAs and a dataDomain specific language (DSL) to parse XTAs from a textual representation. * [`xta-analysis`](../xta-analysis/README.md): XTA specific analysis modules enabling the algorithms to operate on them. ## Using the tool diff --git a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java index f451222c4d..7cfeacdc78 100644 --- a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java +++ b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java @@ -15,20 +15,12 @@ */ package hu.bme.mit.theta.xta.cli; -import java.io.*; -import java.nio.file.Path; -import java.util.concurrent.TimeUnit; - import com.beust.jcommander.JCommander; import com.beust.jcommander.Parameter; import com.beust.jcommander.ParameterException; - import com.google.common.base.Stopwatch; -import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -import hu.bme.mit.theta.analysis.algorithm.SearchStrategy; -import hu.bme.mit.theta.analysis.expl.ExplState; import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; import hu.bme.mit.theta.analysis.unit.UnitPrec; import hu.bme.mit.theta.analysis.utils.ArgVisualizer; @@ -48,34 +40,26 @@ import hu.bme.mit.theta.solver.SolverFactory; import hu.bme.mit.theta.solver.SolverManager; import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; import hu.bme.mit.theta.solver.z3.Z3SolverManager; -import hu.bme.mit.theta.solver.z3.Z3SolverFactory; import hu.bme.mit.theta.xta.XtaSystem; import hu.bme.mit.theta.xta.XtaVisualizer; -import hu.bme.mit.theta.xta.analysis.XtaAction; -import hu.bme.mit.theta.xta.analysis.combinedlazycegar.CombinedLazyCegarXtaCheckerConfigFactory; -import hu.bme.mit.theta.xta.analysis.lazy.*; -import hu.bme.mit.theta.xta.analysis.XtaState; import hu.bme.mit.theta.xta.analysis.config.XtaConfig; -import hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder; +import hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder_Zone; import hu.bme.mit.theta.xta.analysis.lazy.ClockStrategy; -import hu.bme.mit.theta.xta.analysis.lazy.DataStrategy; -import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaCheckerFactory; import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaStatistics; import hu.bme.mit.theta.xta.dsl.XtaDslManager; import hu.bme.mit.theta.xta.utils.CTLOperatorNotSupportedException; import hu.bme.mit.theta.xta.utils.MixedDataTimeNotSupportedException; -import javax.sound.sampled.AudioFormat; +import java.io.*; +import java.nio.file.Path; -import static com.google.common.base.Preconditions.checkNotNull; -import static hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder.*; +import static hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder_Zone.*; public final class XtaCli { public enum Algorithm { - LAZY, EXPERIMENTAL_EAGERLAZY + EAGER } private static final String JAR_NAME = "theta-xta.jar"; @@ -85,7 +69,7 @@ public enum Algorithm { @Parameter(names = {"--model", "-m"}, description = "Path of the input model", required = true) String model; - @Parameter(names = {"--discreteconcr", "-dc"}, description = "Concrete domain for discrete variables", required = false) + /*@Parameter(names = {"--discreteconcr", "-dc"}, description = "Concrete domain for discrete variables", required = false) DataStrategy2.ConcrDom concrDataDom = DataStrategy2.ConcrDom.EXPL; @Parameter(names = {"--discreteabstr", "-da"}, description = "Abstract domain for discrete variables", required = false) @@ -95,20 +79,17 @@ public enum Algorithm { DataStrategy2.ItpStrategy dataItpStrategy = DataStrategy2.ItpStrategy.BIN_BW; @Parameter(names = {"--meet", "-me"}, description = "Meet strategy for expressions", required = false) - ExprMeetStrategy exprMeetStrategy = ExprMeetStrategy.BASIC; + ExprMeetStrategy exprMeetStrategy = ExprMeetStrategy.BASIC;*/ @Parameter(names = {"--clock", "-c"}, description = "Refinement strategy for clock variables", required = false) ClockStrategy clockStrategy = ClockStrategy.BWITP; - @Parameter(names = {"--search", "-s"}, description = "Search strategy", required = false) - SearchStrategy searchStrategy = SearchStrategy.BFS; + @Parameter(names = {"--algorithm"}, description = "") + Algorithm algorithm = Algorithm.EAGER; @Parameter(names = {"--benchmark", "-b"}, description = "Benchmark mode (only print metrics)") Boolean benchmarkMode = false; - @Parameter(names = {"--visualize", "-v"}, description = "Write proof or counterexample to file in dot format") - String dotfile = null; - @Parameter(names = {"--header", "-h"}, description = "Print only a header (for benchmarks)", help = true) boolean headerOnly = false; @@ -122,8 +103,6 @@ public enum Algorithm { boolean versionInfo = false; //Eager CEGAR - @Parameter(names = {"--checkmethod", "-cm"}, description = "Check the model with Eager-CEGAR, or Lazy-Abstraction", required = true) - String method; @Parameter(names = "--domain", description = "Abstract domain") Domain domain = Domain.PRED_CART; @@ -158,10 +137,6 @@ public enum Algorithm { @Parameter(names = "--prunestrategy", description = "Strategy for pruning the ARG after refinement") PruneStrategy pruneStrategy = PruneStrategy.LAZY; - @Parameter(names = "--loglevel", description = "Detailedness of logging") - Logger.Level logLevel = Logger.Level.SUBSTEP; - - @Parameter(names = "--cex", description = "Write concrete counterexample to a file") String cexfile = null; @@ -199,10 +174,6 @@ private void run() { return; } try { - if(method.equals("eager")){ - Eager_Cegar_check(); - return; - } } catch (Throwable ex) { printError(ex); System.exit(1); @@ -221,8 +192,8 @@ private void run() { try { final XtaSystem system = loadModel(); switch (algorithm) { - case LAZY -> runLazy(system); - case EXPERIMENTAL_EAGERLAZY -> runCombined(system); + //case LAZY -> runLazy(system); + //case EXPERIMENTAL_EAGERLAZY -> runCombined(system); case EAGER -> runEager(system); } } catch (final Throwable ex) { @@ -231,7 +202,7 @@ private void run() { } } - private void runLazy(final XtaSystem system) { + /*private void runLazy(final XtaSystem system) { final LazyXtaAbstractorConfig abstractor = LazyXtaAbstractorConfigFactory.create( system, new DataStrategy2(concrDataDom, abstrDataDom, dataItpStrategy), clockStrategy, searchStrategy, exprMeetStrategy @@ -244,16 +215,10 @@ private void runCombined(final XtaSystem system) { final var config = CombinedLazyCegarXtaCheckerConfigFactory.create(system, NullLogger.getInstance(), Z3SolverFactory.getInstance()).build(); final var result = config.check(); resultPrinter(result.isSafe(), result.isUnsafe(), system); - } + }*/ private void runEager(XtaSystem system){ - final SafetyChecker checker = LazyXtaCheckerFactory.create(system, dataStrategy, - clockStrategy, searchStrategy); - final SafetyResult result = check(checker); - resultPrinter(result.isSafe(), result.isUnsafe(), system); - if (dotfile != null) { - writeVisualStatus(result, dotfile); - } + Eager_Cegar_check(system); } private void resultPrinter(final boolean isSafe, final boolean isUnsafe, final XtaSystem system) { @@ -335,7 +300,7 @@ private void writeVisualStatus(final SafetyResult status, final String fil GraphvizWriter.getInstance().writeFile(graph, filename); } - private void Eager_Cegar_check(){ + private void Eager_Cegar_check(XtaSystem xta){ final SolverFactory abstractionSolverFactory; try { SolverManager.registerSolverManager(Z3SolverManager.create()); @@ -346,7 +311,6 @@ private void Eager_Cegar_check(){ } final Stopwatch sw = Stopwatch.createStarted(); - final XtaSystem xta = loadModel(); if (visualize != null) { final Graph graph = XtaVisualizer.visualize(xta); @@ -373,7 +337,7 @@ private void Eager_Cegar_check(){ final XtaConfig configuration = buildConfiguration(xta, abstractionSolverFactory, refinementSolverFactory); final SafetyResult status = check(configuration); sw.stop(); - printResult(status); + resultPrinter(status.isSafe(), status.isUnsafe(), xta); if (status.isUnsafe() && cexfile != null) { writeCex(status.asUnsafe()); } @@ -385,7 +349,7 @@ private void Eager_Cegar_check(){ } private XtaConfig buildConfiguration(final XtaSystem xta, final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) throws Exception { try { - return new XtaConfigBuilder(domain, refinement, abstractionSolverFactory, refinementSolverFactory) + return new XtaConfigBuilder_Zone(domain, refinement, abstractionSolverFactory, refinementSolverFactory) .precGranularity(precGranularity).search(search) .predSplit(predSplit).maxEnum(maxEnum).initPrec(initPrec) .pruneStrategy(pruneStrategy).logger(logger).build(xta); diff --git a/subprojects/xta/xta/README.md b/subprojects/xta/xta/README.md index c30306ba8b..ba598ab5a7 100644 --- a/subprojects/xta/xta/README.md +++ b/subprojects/xta/xta/README.md @@ -1,9 +1,9 @@ ## Overview -This project contains the Uppaal timed automata (XTA) formalism. Its main purpose is to describe timed systems as graphs with clock variables. A domain specific language (DSL) is available to parse XTAs from the textual representation of Uppaal. The project contains: +This project contains the Uppaal timed automata (XTA) formalism. Its main purpose is to describe timed systems as graphs with clock variables. A dataDomain specific language (DSL) is available to parse XTAs from the textual representation of Uppaal. The project contains: * Classes to represent XTAs. -* A domain specific language (DSL) to parse XTAs from a textual representation. +* A dataDomain specific language (DSL) to parse XTAs from a textual representation. ### Related projects diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java index c8b3956682..76275dcf26 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java @@ -110,10 +110,13 @@ public Edge createEdge(final Loc source, final Loc target, final Collection sync, final List updates) { checkArgument(locs.contains(source)); checkArgument(locs.contains(target)); + if(!name.equals("ErrorProc") && !target.getKind().equals(LocKind.ERROR)) { int count = 0; + //this for is to add the update the location bool variables to keep track of which are the active locations (for property checking) for (VarDecl var : system.getDataVars()) { - if (!target.equals(source) || count == 2) { + //count : if we find both of the location bool variable we can break the cycle + if (!target.equals(source) && count < 2) { if (var.getName().contains(target.name)) { updates.add(AssignStmt.create(var, BoolLitExpr.of(true))); count++;