Add integration tests for STSs

subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsTest.java

@@ -0,0 +1,90 @@
+package hu.bme.mit.theta.sts.analysis;
+
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.analysis.State;
+import hu.bme.mit.theta.common.Utils;
+import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.sts.STS;
+import hu.bme.mit.theta.sts.aiger.AigerParser;
+import hu.bme.mit.theta.sts.aiger.AigerToSts;
+import hu.bme.mit.theta.sts.analysis.config.StsConfig;
+import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder;
+import hu.bme.mit.theta.sts.dsl.StsDslManager;
+import hu.bme.mit.theta.sts.dsl.StsSpec;
+import org.junit.Assert;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+
+import java.io.FileInputStream;
+import java.io.IOException;
+import java.util.Arrays;
+import java.util.Collection;
+
+import static hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Domain.*;
+import static hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder.Refinement.SEQ_ITP;
+
+@RunWith(value = Parameterized.class)
+public class StsTest {
+	@Parameterized.Parameter(value = 0)
+	public String filePath;
+
+	@Parameterized.Parameter(value = 1)
+	public StsConfigBuilder.Domain domain;
+
+	@Parameterized.Parameter(value = 2)
+	public StsConfigBuilder.Refinement refinement;
+
+	@Parameterized.Parameter(value = 3)
+	public boolean isSafe;
+
+	@Parameterized.Parameters(name = "{index}: {0}, {1}, {2}, {3}")
+	public static Collection<Object[]> data() {
+		return Arrays.asList(new Object[][]{
+				{ "src/test/resources/hw1_false.aag", PRED_CART, SEQ_ITP, false },
+
+				{ "src/test/resources/hw2_true.aag", PRED_CART, SEQ_ITP, true },
+
+				{ "src/test/resources/boolean1.system", PRED_CART, SEQ_ITP, false },
+
+				{ "src/test/resources/boolean2.system", PRED_CART, SEQ_ITP, false },
+
+				{ "src/test/resources/counter.system", PRED_CART, SEQ_ITP, true },
+
+				{ "src/test/resources/counter_bad.system", PRED_CART, SEQ_ITP, false },
+
+				{ "src/test/resources/counter_parametric.system", PRED_CART, SEQ_ITP, true },
+
+				{ "src/test/resources/loop.system", EXPL, SEQ_ITP, true },
+
+				{ "src/test/resources/loop_bad.system", EXPL, SEQ_ITP, false },
+
+				{ "src/test/resources/multipleinitial.system", PRED_CART, SEQ_ITP, false },
+
+				{ "src/test/resources/readerswriters.system", PRED_CART, SEQ_ITP, true },
+
+				{ "src/test/resources/simple1.system", EXPL, SEQ_ITP, false },
+
+				{ "src/test/resources/simple2.system", EXPL, SEQ_ITP, true },
+
+				{ "src/test/resources/simple3.system", EXPL, SEQ_ITP, false },
+		});
+	}
+
+	@Test
+	public void test() throws IOException {
+		STS sts = null;
+		if (filePath.endsWith("aag")) sts = AigerToSts.createSts(AigerParser.parse(filePath));
+		else {
+			final StsSpec spec = StsDslManager.createStsSpec(new FileInputStream(filePath));
+			if (spec.getAllSts().size() != 1)
+				throw new UnsupportedOperationException("STS contains multiple properties.");
+			sts = Utils.singleElementOf(spec.getAllSts());
+		}
+		StsConfig<? extends State, ? extends Action, ? extends Prec> config
+				= new StsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()).build(sts);
+		Assert.assertEquals(isSafe, config.check().isSafe());
+	}
+
+}

subprojects/sts-analysis/src/test/resources/boolean1.system

@@ -0,0 +1,19 @@
+specification bool1 {
+
+	property safe : {
+		var x1 : bool
+		var x2 : bool
+
+		// This dummy invariant is needed because TTMCInterpolatingSolver throws an exception for an empty list of invariants
+		invariant x1 = x1
+
+		initial not x1
+		initial x2
+		transition x1 or not x2 or x2'
+		transition x1 or x2 or not x1'
+		transition not x1 or x1'
+		transition not x1 or not x2'
+		transition x2 or not x2'
+
+	} models G(not x1 or x2)
+}

subprojects/sts-analysis/src/test/resources/boolean2.system

@@ -0,0 +1,24 @@
+specification bool1 {
+
+	property safe : {
+		var x1 : bool
+		var x2 : bool
+		var x3 : bool
+
+		// This dummy invariant is needed because TTMCInterpolatingSolver throws an exception for an empty list of invariants
+		invariant x1 = x1
+
+		initial not x1
+		initial not x2
+		initial not x3
+
+		transition x1 or not x2'
+		transition x1 or not x2'
+		transition not x1 or x2'
+		transition x2 or not x3'
+		transition not x2 or x3'
+
+	} models
+		G(not x1 or not x2 or not x3)
+
+}

subprojects/sts-analysis/src/test/resources/counter.system

@@ -0,0 +1,11 @@
+specification Counter {
+	property safe : {	
+		var x : int
+		invariant x >= 0
+
+		initial x = 0
+
+		transition if x < 10 then x' = x + 1 or x' = 0 else x' = 0
+
+	} models G(x <= 10)
+}

subprojects/sts-analysis/src/test/resources/counter_bad.system

@@ -0,0 +1,11 @@
+specification Counter {
+	property safe : {	
+		var x : int
+		invariant x >= 0
+
+		initial x = 0
+
+		transition if x < 5 then x' = x + 1 or x' = 0 else x' = 0
+
+	} models G(x < 5)
+}

subprojects/sts-analysis/src/test/resources/counter_parametric.system

@@ -0,0 +1,14 @@
+specification Counter {
+	property safe : {	
+		var x : int
+		var y : int
+		invariant x >= 0
+
+		initial x = 0
+		initial y = 10
+
+		transition if x < y then x' = x + 1 or x' = 0 else x' = 0
+		transition y' = y
+
+	} models G(x <= y)
+}

subprojects/sts-analysis/src/test/resources/hw1_false.aag

@@ -0,0 +1,6 @@
+aag 4 1 3 1 0
+2
+4 2
+6 4
+8 6
+8

subprojects/sts-analysis/src/test/resources/hw2_true.aag

@@ -0,0 +1,5 @@
+aag 3 1 1 1 1
+2
+6 4
+6
+4 2 3

subprojects/sts-analysis/src/test/resources/loop.system

@@ -0,0 +1,30 @@
+// Encoding of the following program:
+// 0. start, x = 0
+// 1. while (x < 5)
+// 2.     x = x + 1
+// 3. end 
+
+specification Program {
+	property s : {
+		var loc : int
+		var x : int
+
+		initial loc = 0
+		initial x = 0
+
+		invariant 0 <= loc and loc <= 3
+
+		invariant x >= 0
+
+		transition loc' =
+			(if loc = 0 then 1
+			else if loc = 1 then (if x < 5 then 2 else 3)
+			else if loc = 2 then 1
+			else loc)
+
+		transition x' =
+			(if loc = 2 then x + 1
+			else x)
+
+	} models G(x <= 5)
+}

subprojects/sts-analysis/src/test/resources/loop_bad.system

@@ -0,0 +1,30 @@
+// Encoding of the following program:
+// 0. start, x = 0
+// 1. while (x < 5)
+// 2.     x = x + 1
+// 3. end 
+
+specification Program {
+	property s : {
+		var loc : int
+		var x : int
+
+		initial loc = 0
+		initial x = 0
+
+		invariant 0 <= loc and loc <= 3
+
+		invariant x >= 0 and x <= 5
+
+		transition loc' =
+			(if loc = 0 then 1
+			else if loc = 1 then (if x < 5 then 2 else 3)
+			else if loc = 2 then 1
+			else loc)
+
+		transition x' =
+			(if loc = 2 then x + 1
+			else x)
+
+	} models G(x < 5)
+}

subprojects/sts-analysis/src/test/resources/multipleinitial.system

@@ -0,0 +1,31 @@
+// A simple example where refinement is potentionally required
+specification Test {
+	property s : {
+		// Variables
+		var x : int
+		var y : int
+		var z : int
+
+		// Invariants
+		invariant x >= 1 and x <= 2
+		invariant y >= 0 and y <= 2
+		invariant z >= 0 and z <= 2
+
+		// Initial values
+		initial (y = 2 and x = 2 and z = 0) or (y = 2 and x = 1 and z = 2)
+
+		// Transitions
+		transition x' = (
+			if (not y < 2) and (not x = 1) then x - 1
+			else x + 1
+		)
+		transition y' = (
+			if y < 2 and x = 1 then y * 2
+			else y - 1
+		)
+		transition z' = (
+			if z < y and z < 2 then z + 1
+			else y
+		)
+	} models G(((not y < 2) or (not x = 1)) and (z=z)) // Does not hold
+}

subprojects/sts-analysis/src/test/resources/readerswriters.system

@@ -0,0 +1,22 @@
+specification PetriNet {
+	property s : {
+		var reading : int
+		var writing : int
+		var idle : int
+
+		initial reading = 0
+		initial writing = 0
+		initial idle = 3
+
+		invariant 0 <= reading and reading <= 3
+		invariant 0 <= writing and writing <= 3
+		invariant 0 <= idle and idle <= 3
+
+		transition
+			(reading > 0 and reading' = reading - 1 and idle' = idle + 1 and writing' = writing) or
+			(writing > 0 and reading' = reading and idle' = idle + 1 and writing' = writing - 1) or
+			(idle > 0 and writing = 0 and reading' = reading + 1 and idle' = idle - 1 and writing' = writing) or
+			(idle > 0 and writing = 0 and reading = 0 and reading' = reading and idle' = idle - 1 and writing' = writing + 1)
+
+	} models G((writing = 0 or reading = 0))
+}

subprojects/sts-analysis/src/test/resources/simple1.system

@@ -0,0 +1,34 @@
+// Simple example from the paper "Counterexample-Guided Abstraction Refinement for Symbolic Model Checking"
+specification Test {
+	property s : {
+		// Variables
+		var reset : int
+		var x : int
+		var y : int
+
+		// Invariants
+		invariant 0 <= reset and reset <= 1
+		invariant 0 <= x and x <= 2
+		invariant 0 <= y and y <= 2
+
+		// Initial values
+		initial reset = 0
+		initial x = 0
+		initial y = 1
+
+		// Transitions
+		transition reset' >= 0 and reset' <= 1
+		transition x' = (
+			if reset = 1 then 0
+			else if x < y then x + 1
+			else if x = y then 0
+			else x
+		)
+		transition y' = (
+			if reset = 1 then 0
+			else if x = y and not y = 2 then y + 1
+			else if x = y then 0
+			else y
+		)
+	} models G(x < y or reset = 1) // Does not hold
+}

subprojects/sts-analysis/src/test/resources/simple2.system

@@ -0,0 +1,33 @@
+// A simple example where refinement is potentionally required
+specification Test {
+	property s : {
+		// Variables
+		var x : int
+		var y : int
+		var z : int
+
+		// Invariants
+		invariant x >= 1 and x <= 2
+		invariant y >= 0 and y <= 2
+		invariant z >= 0 and z <= 2
+
+		// Initial values
+		initial x = 2
+		initial y = 2
+		initial z = 0
+
+		// Transitions
+		transition x' = (
+			if (not y < 2) and (not x = 1) then x - 1
+			else x + 1
+		)
+		transition y' = (
+			if y < 2 and x = 1 then y * 2
+			else y - 1
+		)
+		transition z' = (
+			if z < y and z < 2 then z + 1
+			else y
+		)
+	} models G((not y < 2) or x = 1) // Holds
+}