Merge pull request #75 from ftsrg/xsts

Add XSTS formalism

.github/workflows/docker-tools.yml

@@ -21,6 +21,15 @@ jobs:
     - name: Run STS docker on example
       run: ./docker/run-theta-sts-cli.sh subprojects/sts/src/test/resources/simple1.system
 
+  xsts-cli-docker:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v2
+    - name: Build XSTS Docker image
+      run: docker build -t theta-xsts-cli -f docker/theta-xsts-cli.Dockerfile .
+    - name: Run XSTS docker on example
+      run: ./docker/run-theta-xsts-cli.sh subprojects/xsts-analysis/src/test/resources/model/sequential.xsts --property "!(x==1)"
+
   xta-cli-docker:
     runs-on: ubuntu-latest
     steps:

CONTRIBUTORS.md

@@ -1,10 +1,10 @@
 # Contributors to Theta
-* [Tamás Tóth](https://inf.mit.bme.hu/en/members/totht) [1]
-* [Ákos Hajdu](https://inf.mit.bme.hu/en/members/hajdua) [1] [2]
-* [Gábor Szárnyas](https://inf.mit.bme.hu/en/members/szarnyasg) [1] [2]
-* [Kristóf Marussy](https://inf.mit.bme.hu/en/members/marussyk) [1] [2]
-* Mihály Dobos-Kovács [1]
 
-
-1. [Fault Tolerant Systems Research Group](https://inf.mit.bme.hu/en), [Department of Measurement and Information Systems](http://www.mit.bme.hu/eng/), [Budapest University of Technology and Economics](http://www.bme.hu/?language=en)
-2. [MTA-BME Lendület Cyber-Physical Systems Research Group](http://lendulet.inf.mit.bme.hu/)
+Initial design and implementation by [Tamás Tóth](https://inf.mit.bme.hu/en/members/totht) and [Ákos Hajdu](https://hajduakos.github.io).
+
+Contributors:
+* [Gábor Szárnyas](https://inf.mit.bme.hu/en/members/szarnyasg)
+* [Kristóf Marussy](https://inf.mit.bme.hu/en/members/marussyk)
+* Levente Bajczi
+* Mihály Dobos-Kovács
+* Milán Mondok

README.md

@@ -17,15 +17,16 @@ Theta can both serve as a model checking backend, and also includes ready-to-use
 ## Use Theta
 
 Tools are concrete instantiations of the framework to solve a certain problem using the built-in algorithms.
-Currently, the following 3 tools are available.
-Follow the links for more information about each tool.
+Currently, the following tools are available (follow the links for more information).
 
 * [`theta-cfa-cli`](subprojects/cfa-cli): Reachability checking of error locations in Control Flow Automata (CFA) using CEGAR-based algorithms.
-  * [Gazer](https://github.com/FTSRG/gazer) is an [LLVM](https://llvm.org/)-based frontend to verify C programs using theta-cfa-cli.
+  * [Gazer](https://github.com/ftsrg/gazer) is an [LLVM](https://llvm.org/)-based frontend to verify C programs using theta-cfa-cli.
   * [PLCverif](https://cern.ch/plcverif) is a tool developed at CERN for the formal specification and verification of PLC (Programmable Logic Controller) programs, supporting theta-cfa-cli as one of its verification backends.
 * [`theta-sts-cli`](subprojects/sts-cli): Verification of safety properties in Symbolic Transition Systems (STS) using CEGAR-based algorithms.
   * theta-sts-cli natively supports the [AIGER format](http://fmv.jku.at/aiger/) of the [Hardware Model Checking Competition (HWMCC)](http://fmv.jku.at/hwmcc/).
 * [`theta-xta-cli`](subprojects/xta-cli): Verification of [Uppaal](http://www.uppaal.org/) timed automata (XTA).
+* [`theta-xsts-cli`](subprojects/xsts-cli): Verification of safety properties in eXtended Symbolic Transition Systems (XSTS) using CEGAR-based algorithms.
+  * [Gamma](https://github.com/ftsrg/gamma) is a statechart composition framework, that supports theta-xsts-cli as a backend to verify collaborating state machines.
 
 ## Overview of the architecture
 
@@ -35,7 +36,7 @@ Theta can be divided into the following four layers.
 Formalisms are usually low level, mathematical representations based on first order logic expressions and graph like structures.
 Formalisms can also support higher level languages that can be mapped to that particular formalism by a language front-end (consisting of a specific parser and possibly reductions for simplification of the model).
 The common features of the different formalisms reside in the [`core`](subprojects/core) project (e.g., expressions and statements) and each formalism has its own project.
-Currently, there are three formalisms: symbolic transition systems ([`sts`](subprojects/sts)), control-flow automata ([`cfa`](subprojects/cfa)) and timed automata ([`xta`](subprojects/xta)).
+Currently, the following formalisms are supported: (extended) symbolic transition systems ([`sts`](subprojects/sts) / [`xsts`](subprojects/xsts)), control-flow automata ([`cfa`](subprojects/cfa)) and timed automata ([`xta`](subprojects/xta)).
 * **Analysis back-end**: The analysis back-end provides the verification algorithms that can formally prove whether a model meets certain requirements.
 There is an interpreter for each formalism, providing a common interface towards the algorithms (e.g., calculating initial states and successors).
 This ensures that most components of the algorithms work for all formalisms (as long as they provide the interpreter).
@@ -45,18 +46,18 @@ The common components reside in the [`analysis`](subprojects/analysis) project (
 * **SMT solver interface and SMT solvers**: Many components of the algorithms rely on satisfiability modulo theories (SMT) solvers.
 The framework provides a general SMT solver interface in the project [`solver`](subprojects/solver) that supports incremental solving, unsat cores, and the generation of binary and sequence interpolants.
 Currently, the interface is implemented by the [Z3](https://github.com/Z3Prover/z3) SMT solver in the project [`solver-z3`](subprojects/solver-z3), but it can easily be extended with new solvers.
-* **Tools**: Tools are command line or GUI applications that can be compiled into a runnable jar file.
+* **Tools**: Tools are command line applications that can be compiled into a runnable jar file.
 Tools usually read some input and then instantiate and run the algorithms.
-Tools are implemented in separate projects.
+Tools are implemented in separate projects, currently with the `-cli` suffix.
 
 The table below shows the architecture and the projects.
 Each project contains a README.md in its root directory describing its purpose in more detail.
 
-|  | Common | CFA | STS | XTA |
-|--|--|--|--|--|
-| **Tools** |  | [`cfa-cli`](subprojects/cfa-cli) | [`sts-cli`](subprojects/sts-cli) | [`xta-cli`](subprojects/xta-cli) |
-| **Analyses** | [`analysis`](subprojects/analysis) | [`cfa-analysis`](subprojects/cfa-analysis) | [`sts-analysis`](subprojects/sts-analysis) | [`xta-analysis`](subprojects/xta-analysis) |
-| **Formalisms** | [`core`](subprojects/core), [`common`](subprojects/common) | [`cfa`](subprojects/cfa) | [`sts`](subprojects/sts) | [`xta`](subprojects/xta) |
+|  | Common | CFA | STS | XTA | XSTS |
+|--|--|--|--|--|--|
+| **Tools** |  | [`cfa-cli`](subprojects/cfa-cli) | [`sts-cli`](subprojects/sts-cli) | [`xta-cli`](subprojects/xta-cli) | [`xsts-cli`](subprojects/xsts-cli) |
+| **Analyses** | [`analysis`](subprojects/analysis) | [`cfa-analysis`](subprojects/cfa-analysis) | [`sts-analysis`](subprojects/sts-analysis) | [`xta-analysis`](subprojects/xta-analysis) | [`xsts-analysis`](subprojects/xsts-analysis) |
+| **Formalisms** | [`core`](subprojects/core), [`common`](subprojects/common) | [`cfa`](subprojects/cfa) | [`sts`](subprojects/sts) | [`xta`](subprojects/xta) | [`xsts`](subprojects/xsts) |
 | **SMT solvers** | [`solver`](subprojects/solver), [`solver-z3`](subprojects/solver-z3) |
 
 ## Extend Theta
@@ -67,8 +68,9 @@ If you want to extend Theta and build your own algorithms and tools, then take l
 
 If you want to read more, take a look at [our list of publications](https://ftsrg.github.io/theta/publications/).
 A good starting point is our [tool paper](https://ftsrg.github.io/theta/publications/fmcad2017.pdf) and [slides](https://www.slideshare.net/AkosHajdu/theta-a-framework-for-abstraction-refinementbased-model-checking)/[talk](https://oc-presentation.ltcc.tuwien.ac.at/engage/theodul/ui/core.html?id=c658c37e-ae70-11e7-a0dd-bb49f3cb440c) presented at FMCAD 2017.
+Furthermore, our [paper in the Journal of Automated Reasoning](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) is a good overview of the algorithms in Theta.
 
-To cite Theta, please use the following paper.
+To cite Theta as a tool, please use the following paper.
 
 ```
 @inproceedings{theta-fmcad2017,

build.gradle.kts

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

doc/Coding-conventions.md

@@ -7,7 +7,7 @@ We mainly follow the standard Java coding conventions and most of the convention
 
 ## Naming and formatting
 
-* **DO** use the generally accepted naming and source code formatting conventions of Java (Item 56 of [1], Chapter 1 of [5]). If you are developing in Eclipse you can import our commonly used formatting profile (see [For-developers.md](For-developers.md) for more information).
+* **DO** use the generally accepted naming and source code formatting conventions of Java (Item 56 of [1], Chapter 1 of [5]). If you are developing in IntelliJ Idea you can import our commonly used formatting profile (see [Development.md](Development.md) for more information).
 * **DO** start project names with the prefix `hu.bme.mit.theta`.
 * **DO** use CamelCase for class names containing subsequent capital letters, except when the whole name is a sequence of capital letters. Examples: `CFA`, `CfaEdge`, `OsHelper`.
 * **CONSIDER** using abbreviations for well known and common names. Examples: `Expression` -> `Expr`, `Statement` -> `Stmt`, `Counterexample` -> `Cex`.

docker/run-theta-xsts-cli.sh

@@ -0,0 +1,17 @@
+#!/bin/bash
+
+set -Eeuxo pipefail
+
+DOCKER_RUN_OPTIONS="-i"
+
+# Only allocate tty if we detect one
+if [ -t 0 ] && [ -t 1 ]; then
+    DOCKER_RUN_OPTIONS="$DOCKER_RUN_OPTIONS -t"
+fi
+
+ABSPATH=$(realpath "$1")
+DIR=$(dirname "$ABSPATH")
+FILE=/host/$(basename "$ABSPATH")
+shift
+
+docker run "$DOCKER_RUN_OPTIONS" --mount type=bind,source="$DIR",target=/host theta-xsts-cli:latest --model "$FILE" "$@"

docker/theta-xsts-cli.Dockerfile

@@ -0,0 +1,16 @@
+FROM openjdk:11.0.6-slim
+
+RUN apt-get update && \
+    apt-get install -y --no-install-recommends libgomp1 && \
+    apt-get clean && rm -rf /var/lib/apt/lists/*
+
+RUN mkdir theta
+COPY . theta
+WORKDIR /theta
+RUN ./gradlew clean && \
+    ./gradlew theta-xsts-cli:build && \
+    mv subprojects/xsts-cli/build/libs/theta-xsts-cli-*-all.jar /theta-xsts-cli.jar
+WORKDIR /
+
+ENV LD_LIBRARY_PATH="$LD_LIBRARY_PATH:./theta/lib/"
+ENTRYPOINT ["java", "-jar", "theta-xsts-cli.jar"]

settings.gradle.kts

@@ -14,7 +14,10 @@ include(
         "sts-cli",
         "xta",
         "xta-analysis",
-        "xta-cli"
+        "xta-cli",
+        "xsts",
+        "xsts-analysis",
+        "xsts-cli"
 )
 
 for (project in rootProject.children) {

subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/StmtApplier.java

@@ -15,13 +15,10 @@
  */
 package hu.bme.mit.theta.analysis.expl;
 
+import hu.bme.mit.theta.core.decl.Decl;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.model.MutableValuation;
-import hu.bme.mit.theta.core.stmt.AssignStmt;
-import hu.bme.mit.theta.core.stmt.AssumeStmt;
-import hu.bme.mit.theta.core.stmt.HavocStmt;
-import hu.bme.mit.theta.core.stmt.SkipStmt;
-import hu.bme.mit.theta.core.stmt.Stmt;
+import hu.bme.mit.theta.core.stmt.*;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.LitExpr;
 import hu.bme.mit.theta.core.type.abstracttype.EqExpr;
@@ -32,6 +29,9 @@
 import hu.bme.mit.theta.core.type.booltype.NotExpr;
 import hu.bme.mit.theta.core.utils.ExprUtils;
 
+import java.util.ArrayList;
+import java.util.List;
+
 final class StmtApplier {
 
 	public enum ApplyResult {
@@ -53,6 +53,15 @@ public static ApplyResult apply(final Stmt stmt, final MutableValuation val, fin
 			return applyHavoc(havocStmt, val);
 		} else if (stmt instanceof SkipStmt) {
 			return applySkip();
+		} else if (stmt instanceof SequenceStmt) {
+			final SequenceStmt sequenceStmt = (SequenceStmt) stmt;
+			return applySequence(sequenceStmt, val, approximate);
+		} else if (stmt instanceof NonDetStmt) {
+			final NonDetStmt nonDetStmt = (NonDetStmt) stmt;
+			return applyNonDet(nonDetStmt, val, approximate);
+		} else if (stmt instanceof OrtStmt) {
+			final OrtStmt ortStmt = (OrtStmt) stmt;
+			return applyOrt(ortStmt, val, approximate);
 		} else {
 			throw new UnsupportedOperationException("Unhandled statement: " + stmt);
 		}
@@ -149,4 +158,59 @@ private static ApplyResult applySkip() {
 		return ApplyResult.SUCCESS;
 	}
 
+	private static ApplyResult applySequence(final SequenceStmt stmt, final MutableValuation val,
+											 final boolean approximate) {
+		MutableValuation copy = MutableValuation.copyOf(val);
+		for(Stmt subStmt: stmt.getStmts()){
+			ApplyResult res=apply(subStmt,copy,approximate);
+			if(res==ApplyResult.BOTTOM || res==ApplyResult.FAILURE) return res;
+		}
+		val.clear();
+		val.putAll(copy);
+		return ApplyResult.SUCCESS;
+	}
+
+	private static ApplyResult applyNonDet(final NonDetStmt stmt, final MutableValuation val,
+											 final boolean approximate) {
+		List<MutableValuation> valuations=new ArrayList<MutableValuation>();
+		int successIndex=-1;
+		for(int i=0; i<stmt.getStmts().size(); i++){
+			MutableValuation subVal=MutableValuation.copyOf(val);
+			ApplyResult res=apply(stmt.getStmts().get(i),subVal,approximate);
+			if(res==ApplyResult.FAILURE) return ApplyResult.FAILURE;
+			if(res==ApplyResult.SUCCESS){
+				valuations.add(subVal);
+				if(successIndex==-1)successIndex=i;
+			}
+		}
+		if(valuations.size()==0){
+			return ApplyResult.BOTTOM;
+		} else  if(valuations.size()==1){
+			return apply(stmt.getStmts().get(successIndex),val,approximate);
+		} else if(approximate){
+			apply(stmt.getStmts().get(successIndex),val,approximate);
+			List<Decl> toRemove=new ArrayList<Decl>();
+			for(Decl decl: val.getDecls()){
+				for(MutableValuation subVal: valuations){
+					if(!val.eval(decl).equals(subVal.eval(decl))){
+						toRemove.add(decl);
+						break;
+					}
+				}
+			}
+			for(Decl decl:toRemove) val.remove(decl);
+			return ApplyResult.SUCCESS;
+		} else{
+			return ApplyResult.FAILURE;
+		}
+	}
+
+	private static ApplyResult applyOrt(final OrtStmt stmt, final MutableValuation val,
+										   final boolean approximate) {
+		throw new UnsupportedOperationException();
+	}
+
+
+
+
 }

subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/DefaultPreStrengtheningOperator.java

@@ -0,0 +1,28 @@
+package hu.bme.mit.theta.analysis.prod2;
+
+import hu.bme.mit.theta.analysis.State;
+
+import static com.google.common.base.Preconditions.checkNotNull;
+
+public class DefaultPreStrengtheningOperator<S1 extends State, S2 extends State> implements PreStrengtheningOperator<S1, S2> {
+
+    private DefaultPreStrengtheningOperator(){}
+
+    public static <S1 extends State, S2 extends State> PreStrengtheningOperator<S1, S2> create(){
+        return new DefaultPreStrengtheningOperator<>();
+    }
+
+    @Override
+    public S1 strengthenState1(Prod2State<S1, S2> state) {
+        checkNotNull(state);
+
+        return state.getState1();
+    }
+
+    @Override
+    public S2 strengthenState2(Prod2State<S1, S2> state) {
+        checkNotNull(state);
+
+        return state.getState2();
+    }
+}

subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/PreStrengtheningOperator.java

@@ -0,0 +1,11 @@
+package hu.bme.mit.theta.analysis.prod2;
+
+import hu.bme.mit.theta.analysis.State;
+
+public interface PreStrengtheningOperator<S1 extends State, S2 extends State> {
+
+    S1 strengthenState1(final Prod2State<S1, S2> state);
+
+    S2 strengthenState2(final Prod2State<S1, S2> state);
+
+}

subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/prod2/Prod2Analysis.java

@@ -33,23 +33,25 @@ public final class Prod2Analysis<S1 extends State, S2 extends State, A extends A
 	private final TransFunc<Prod2State<S1, S2>, A, Prod2Prec<P1, P2>> transFunc;
 
 	private Prod2Analysis(final Analysis<S1, ? super A, P1> analysis1, final Analysis<S2, ? super A, P2> analysis2,
+						  final PreStrengtheningOperator<S1, S2> preStrengtheningOperator,
 						  final StrengtheningOperator<S1, S2, P1, P2> strenghteningOperator) {
 		checkNotNull(analysis1);
 		checkNotNull(analysis2);
 		partialOrd = Prod2Ord.create(analysis1.getPartialOrd(), analysis2.getPartialOrd());
 		initFunc = Prod2InitFunc.create(analysis1.getInitFunc(), analysis2.getInitFunc(), strenghteningOperator);
-		transFunc = Prod2TransFunc.create(analysis1.getTransFunc(), analysis2.getTransFunc(), strenghteningOperator);
+		transFunc = Prod2TransFunc.create(analysis1.getTransFunc(), analysis2.getTransFunc(), preStrengtheningOperator, strenghteningOperator);
 	}
 
 	public static <S1 extends State, S2 extends State, A extends Action, P1 extends Prec, P2 extends Prec> Prod2Analysis<S1, S2, A, P1, P2> create(
 			final Analysis<S1, ? super A, P1> analysis1, final Analysis<S2, ? super A, P2> analysis2) {
-		return create(analysis1, analysis2, (states, prec) -> states);
+		return create(analysis1, analysis2, DefaultPreStrengtheningOperator.create(), (states, prec) -> states);
 	}
 
 	public static <S1 extends State, S2 extends State, A extends Action, P1 extends Prec, P2 extends Prec> Prod2Analysis<S1, S2, A, P1, P2> create(
 			final Analysis<S1, ? super A, P1> analysis1, final Analysis<S2, ? super A, P2> analysis2,
+			final PreStrengtheningOperator<S1, S2> preStrengtheningOperator,
 			final StrengtheningOperator<S1, S2, P1, P2> strenghteningOperator) {
-		return new Prod2Analysis<>(analysis1, analysis2, strenghteningOperator);
+		return new Prod2Analysis<>(analysis1, analysis2, preStrengtheningOperator, strenghteningOperator);
 	}
 
 	@Override