From ae8bd861bcecc93bb7d81a4445458aae74f82c0c Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 17 Nov 2022 10:13:00 +0100 Subject: [PATCH 1/3] Changed naming to testBound --- README.md | 16 ++++++++-------- src/main/kotlin/Main.kt | 10 +++++----- src/main/kotlin/parsing/EngineConfiguration.kt | 2 +- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index a618a19..dad808f 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ Requires a configuration file `configuration.json` with information for each eng "enabled" : true, "verbose": true, "testTimeout": 30, - "testCount" : 4000, + "testBound" : 4000, "testSorting": "Random", "queryComplexity": [0, 1000], "testsSavePath": "/path/to/file" @@ -42,14 +42,14 @@ Requires a configuration file `configuration.json` with information for each eng ``` If an `executablePath` or `parameterExpression` is omitted, the engine is expected to be hosted externally. An example of this is the `External` engine in the above configuration. Engines can optionally be marked `verbose` to print failed queries while the tests are run from [Run Tests for Engine](#run-tests-for-engine) -`testTimeout`, `testCount`, `testSorting`, `queryComplexity`, and `testsSavePath` are all optional attributes. +`testTimeout`, `testBound`, `testSorting`, `queryComplexity`, and `testsSavePath` are all optional attributes. `testTimeout` sets the time limit in seconds for the duration of a test (default=30). -`testCount` limits the number of tests to execute (default=all). -`testSorting` determines how to sort the tests if `testCount` is set. There are four different sortings: -* `Random` (default) - Takes `testCount` generated tests randomly -* `FILO` - Takes the last `testCount` generated tests -* `FIFO` - Takes the first `testCount` generated tests -* `Split` - Takes an equal split of each test-sort by RoundRobin, summing up to no more than `testCount` tests +`testBound` sets an upper bound of the number of tests to execute (default=all). +`testSorting` determines how to sort the tests if `testBound` is set. There are four different sortings: +* `Random` (default) - Takes `testBound` generated tests randomly +* `FILO` - Takes the last `testBound` generated tests +* `FIFO` - Takes the first `testBound` generated tests +* `Split` - Takes an equal split of each test-sort by RoundRobin, summing up to no more than `testBound` tests `queryComplexity` determines the complexity of the queries in the tests (the number of operators). Both the upper and lower bound can be set. diff --git a/src/main/kotlin/Main.kt b/src/main/kotlin/Main.kt index 11a9f4d..284a762 100644 --- a/src/main/kotlin/Main.kt +++ b/src/main/kotlin/Main.kt @@ -121,12 +121,12 @@ private fun sortTests(engine: EngineConfiguration, tests: Collection) : Co }) } - if (engine.testCount != null) { //Count + if (engine.testBound != null) { //Count out = when (engine.testSorting) { - Sorting.FILO -> ArrayList(out.takeLast(engine.testCount)) - Sorting.FIFO -> ArrayList(out.take(engine.testCount)) - Sorting.RoundRobin -> getEqualTests(out, engine.testCount) - Sorting.Random, null -> ArrayList(out.shuffled().take(engine.testCount)) + Sorting.FILO -> ArrayList(out.takeLast(engine.testBound)) + Sorting.FIFO -> ArrayList(out.take(engine.testBound)) + Sorting.RoundRobin -> getEqualTests(out, engine.testBound) + Sorting.Random, null -> ArrayList(out.shuffled().take(engine.testBound)) } } return out diff --git a/src/main/kotlin/parsing/EngineConfiguration.kt b/src/main/kotlin/parsing/EngineConfiguration.kt index 9e50f86..1ade727 100644 --- a/src/main/kotlin/parsing/EngineConfiguration.kt +++ b/src/main/kotlin/parsing/EngineConfiguration.kt @@ -27,7 +27,7 @@ data class EngineConfiguration ( val addresses: List = (port until port + processes).map { "${ip}:$it" }, val ports: List = (port until port + processes).toList(), @Json(serializeNull = false) - val testCount: Int?, + val testBound: Int?, @Json(serializeNull = false) val testSorting: Sorting?, @Json(serializeNull = false) From d77cbdabbc911b4533adef8f8672393b7571d81c Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Tue, 29 Nov 2022 15:36:04 +0100 Subject: [PATCH 2/3] Annotates system and tests with related proofs --- logs.txt | 96 +++++++++++++++++++ src/main/kotlin/Main.kt | 23 ++++- .../kotlin/parsing/EngineConfiguration.kt | 5 +- src/main/kotlin/parsing/System.kt | 11 ++- .../kotlin/proofs/ConsistentCompositions.kt | 4 + .../kotlin/proofs/ConsistentRefinements.kt | 3 + src/main/kotlin/proofs/ContextSwitch.kt | 6 +- src/main/kotlin/proofs/Proof.kt | 16 +++- src/main/kotlin/proofs/QuotientRule.kt | 17 ++-- .../kotlin/proofs/RefinementTransitivity.kt | 4 + src/main/kotlin/proofs/SelfRefinement.kt | 2 + src/main/kotlin/proofs/Theorem6Conj1.kt | 3 + src/main/kotlin/proofs/Theorem6Conj2.kt | 3 + src/main/kotlin/tests/ImplicationTest.kt | 6 +- src/main/kotlin/tests/NotSatisfiedTest.kt | 3 +- src/main/kotlin/tests/SatisfiedTest.kt | 3 +- src/main/kotlin/tests/Test.kt | 8 +- .../ConjunctionCommutativeTests.kt | 3 +- .../ConjunctionIdentityTests.kt | 8 +- .../tests/testgeneration/ConsistencyTests.kt | 6 +- .../testgeneration/ImpliedRefinementTest.kt | 13 ++- .../tests/testgeneration/NotRefinement.kt | 3 +- .../tests/testgeneration/RefinementTests.kt | 6 +- 23 files changed, 219 insertions(+), 33 deletions(-) create mode 100644 logs.txt diff --git a/logs.txt b/logs.txt new file mode 100644 index 0000000..05f66d3 --- /dev/null +++ b/logs.txt @@ -0,0 +1,96 @@ +Tests generated for engine 'Reveaal' on 29/11/2022 03:18:43 +----------------------------------------------------------- + +samples/json/EcdarUniversity + ImplicationTest: ImpliedRefinement + "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((Adm2 && HalfAdm1) || Researcher) && ((Adm2 && HalfAdm2) || Researcher) && (Adm2 || Researcher)) \\ Adm2)" + "refinement: Researcher <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((Adm2 && HalfAdm1) || Researcher) && ((Adm2 && HalfAdm2) || Researcher) && (Adm2 || Researcher)) \\ Adm2)" + ImplicationTest: ImpliedSelfRefinement + "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2))" + "refinement: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2)) <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2))" + ImplicationTest: ImpliedRefinement + "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Researcher)" + "refinement: Machine <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Researcher)" + ImplicationTest: ImpliedSelfRefinement + "consistency: (((Administration || Machine || Researcher) \\ Administration) \\ Researcher)" + "refinement: (((Administration || Machine || Researcher) \\ Administration) \\ Researcher) <= (((Administration || Machine || Researcher) \\ Administration) \\ Researcher)" + ImplicationTest: ImpliedSelfRefinement + "consistency: (((HalfAdm1 && HalfAdm2) || Researcher) \\ (Adm2 && HalfAdm2))" + "refinement: (((HalfAdm1 && HalfAdm2) || Researcher) \\ (Adm2 && HalfAdm2)) <= (((HalfAdm1 && HalfAdm2) || Researcher) \\ (Adm2 && HalfAdm2))" + ImplicationTest: ImpliedSelfRefinement + "consistency: (((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) \\ Adm2)" + "refinement: (((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) \\ Adm2) <= (((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) \\ Adm2)" + ImplicationTest: ImpliedSelfRefinement + "consistency: (((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm1) || Machine))" + "refinement: (((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm1) || Machine)) <= (((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm1) || Machine))" + ImplicationTest: ImpliedRefinement + "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ (Adm2 && HalfAdm1))" + "refinement: Researcher <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ (Adm2 && HalfAdm1))" + ImplicationTest: ImpliedSelfRefinement + "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ (Adm2 && HalfAdm1))" + "refinement: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ (Adm2 && HalfAdm1)) <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ (Adm2 && HalfAdm1))" + ImplicationTest: ImpliedRefinement + "consistency: (((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((Adm2 && HalfAdm1) || Researcher))" + "refinement: ((HalfAdm1 && HalfAdm2) || Researcher) <= (((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((Adm2 && HalfAdm1) || Researcher))" + ImplicationTest: ImpliedRefinement + "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((HalfAdm1 && HalfAdm2) || Researcher) && (Adm2 || Researcher)) \\ (Adm2 && HalfAdm2))" + "refinement: Researcher <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((HalfAdm1 && HalfAdm2) || Researcher) && (Adm2 || Researcher)) \\ (Adm2 && HalfAdm2))" + ImplicationTest: ImpliedSelfRefinement + "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Machine)" + "refinement: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Machine) <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Machine)" + ImplicationTest: ImpliedSelfRefinement + "consistency: ((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Adm2)" + "refinement: ((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Adm2) <= ((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Adm2)" + ImplicationTest: ImpliedRefinement + "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ Researcher)" + "refinement: (HalfAdm1 && HalfAdm2) <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ Researcher)" + NotSatisfiedTest: NotRefines + "refinement: Researcher <= ((Spec \\ Machine) \\ (Adm2 && HalfAdm1 && HalfAdm2))" + ImplicationTest: ImpliedRefinement + "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2))" + "refinement: (Machine || Researcher) <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2))" + ImplicationTest: ImpliedRefinement + "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher)) \\ (HalfAdm1 && HalfAdm2))" + "refinement: (Machine || Researcher) <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher)) \\ (HalfAdm1 && HalfAdm2))" + ImplicationTest: ImpliedRefinement + "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1))" + "refinement: Machine <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1))" + ImplicationTest: ImpliedRefinement + "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm2) || Machine) && ((HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ Adm2)" + "refinement: Machine <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm2) || Machine) && ((HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ Adm2)" + ImplicationTest: ImpliedRefinement + "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Machine) \\ (HalfAdm1 && HalfAdm2))" + "refinement: Researcher <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Machine) \\ (HalfAdm1 && HalfAdm2))" + ImplicationTest: ImpliedRefinement + "consistency: (Adm2 && HalfAdm1 && HalfAdm2)" + "refinement: (HalfAdm1 && HalfAdm2) <= (Adm2 && HalfAdm1 && HalfAdm2)" + ImplicationTest: ImpliedSelfRefinement + "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2)) \\ Researcher)" + "refinement: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2)) \\ Researcher) <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2)) \\ Researcher)" + ImplicationTest: ImpliedRefinement + "consistency: (((((Adm2 && HalfAdm1) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1)) \\ Machine)" + "refinement: Researcher <= (((((Adm2 && HalfAdm1) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1)) \\ Machine)" + ImplicationTest: ImpliedRefinement + "consistency: (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ (Adm2 && HalfAdm1 && HalfAdm2))" + "refinement: Researcher <= (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ (Adm2 && HalfAdm1 && HalfAdm2))" + ImplicationTest: ImpliedSelfRefinement + "consistency: (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2))" + "refinement: (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2)) <= (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2))" + +samples/xml/delayRefinement.xml + ImplicationTest: ImpliedRefinement + "consistency: (K5 && Z2)" + "refinement: (K5 && Z2) <= K5" + SatisfiedTest: Consistency + "consistency: (F1 || F2)" + ImplicationTest: ImpliedRefinement + "consistency: (K4 && P0)" + "refinement: (K4 && P0) <= K4" + ImplicationTest: ImpliedRefinement + "consistency: (L4 && P6)" + "refinement: (L4 && P6) <= L4" + +samples/json/Conjunction + SatisfiedTest: SelfRefinement + "refinement: Test4 <= Test4" + diff --git a/src/main/kotlin/Main.kt b/src/main/kotlin/Main.kt index 284a762..11b77f9 100644 --- a/src/main/kotlin/Main.kt +++ b/src/main/kotlin/Main.kt @@ -5,6 +5,7 @@ import facts.RelationLoader import parsing.EngineConfiguration import parsing.Sorting import parsing.parseEngineConfigurations +import proofs.ProofKind import proofs.addAllProofs import tests.Test import tests.testgeneration.addAllTests @@ -104,6 +105,14 @@ private fun executeTests(engine: EngineConfiguration, tests: Collection) { private fun generateTests(): Collection { val allRelations = ProofSearcher().addAllProofs().findNewRelations(RelationLoader.relations) //ProofLimiter(3).limit(allRelations) +/* + allRelations.forEach { + println(it) + } + + println(allRelations.size) + println(RelationLoader.relations.size) + */ return TestGenerator().addAllTests().generateTests(allRelations) } @@ -111,6 +120,17 @@ private fun sortTests(engine: EngineConfiguration, tests: Collection) : Co val operators = listOf("||", "\\\\", "&&", "consistency:", "refinement:") var out = ArrayList(tests) + println("Test count: " + out.size) + engine.blackList?.let { it -> + val blacklisting = it.sumOf {it.value} + println(blacklisting) + // TODO: Check should be fixed + // This removes a test even if it has only one match. Not sure if this is a desired outcome + out = ArrayList(out.filter { test -> test.relatedProofs and blacklisting == 0}) + //out = ArrayList(out.filter { test -> test.relatedProofs and blacklisting != test.relatedProofs}) + } + println("Test count: " + out.size) + if (engine.queryComplexity != null) { //Query Complexity val (lower, upper) = engine.bounds() @@ -121,7 +141,7 @@ private fun sortTests(engine: EngineConfiguration, tests: Collection) : Co }) } - if (engine.testBound != null) { //Count + if (engine.testBound != null) { //Bound out = when (engine.testSorting) { Sorting.FILO -> ArrayList(out.takeLast(engine.testBound)) Sorting.FIFO -> ArrayList(out.take(engine.testBound)) @@ -129,6 +149,7 @@ private fun sortTests(engine: EngineConfiguration, tests: Collection) : Co Sorting.Random, null -> ArrayList(out.shuffled().take(engine.testBound)) } } + return out } diff --git a/src/main/kotlin/parsing/EngineConfiguration.kt b/src/main/kotlin/parsing/EngineConfiguration.kt index 1ade727..6b071b2 100644 --- a/src/main/kotlin/parsing/EngineConfiguration.kt +++ b/src/main/kotlin/parsing/EngineConfiguration.kt @@ -2,6 +2,7 @@ package parsing import com.beust.klaxon.Json import com.beust.klaxon.Klaxon +import proofs.ProofKind import java.io.File import java.io.IOException import java.net.ServerSocket @@ -36,6 +37,8 @@ data class EngineConfiguration ( val deadline: Long?, @Json(serializeNull = false) val testsSavePath: String?, + @Json(serializeNull = false) + val blackList: List?, ) { private var procs : MutableList? = null var alive : AtomicBoolean = AtomicBoolean(true) @@ -140,7 +143,7 @@ data class EngineConfiguration ( return path == null || parameterExpression == null } - public fun bounds(): Pair { + fun bounds(): Pair { val upper: Int; val lower: Int if (this.queryComplexity!!.size >= 2) { upper = this.queryComplexity[1] diff --git a/src/main/kotlin/parsing/System.kt b/src/main/kotlin/parsing/System.kt index 2ee20c0..e6087bf 100644 --- a/src/main/kotlin/parsing/System.kt +++ b/src/main/kotlin/parsing/System.kt @@ -3,6 +3,7 @@ package parsing import facts.RelationLoader.getInputs import facts.RelationLoader.getOutputs import facts.RelationLoader.prefixMap +import proofs.ProofKind import java.util.* interface System { @@ -18,6 +19,7 @@ interface System { var isLocallyConsistent: Optional var inputs: HashSet var outputs: HashSet + var relatedProofs: Int fun isKnownLocallyConsistent(): Boolean { return isLocallyConsistent.orElse(false) @@ -82,6 +84,7 @@ class Component(val prefix: String, val comp: String) : System { get() = 0 override var components = 1 override var isLocallyConsistent: Optional = Optional.empty() + override var relatedProofs: Int = 0 override fun sameAs(other: System): Boolean { @@ -125,6 +128,8 @@ class Quotient(var T: System, var S: System) : System { override var notRefinesThis = HashSet() override var thisNotRefines = HashSet() override var parents = HashSet() + override var relatedProofs: Int = 0 + override val depth: Int get() = 1 + (this.children.map { it.depth }.maxOrNull() ?: 0) override val components: Int @@ -230,7 +235,9 @@ class Quotient(var T: System, var S: System) : System { override var notRefinesThis = HashSet() override var thisNotRefines = HashSet() override var parents = HashSet() - override val depth: Int + override var relatedProofs: Int = 0 + + override val depth: Int get() = 1 + (this.children.map { it.depth }.maxOrNull() ?: 0) override val components: Int get() = children.sumOf { it.components } @@ -332,6 +339,8 @@ class Composition : System { override var notRefinesThis = HashSet() override var thisNotRefines = HashSet() override var parents = HashSet() + override var relatedProofs: Int = 0 + override val components: Int get() = children.sumOf { it.components } override val depth: Int diff --git a/src/main/kotlin/proofs/ConsistentCompositions.kt b/src/main/kotlin/proofs/ConsistentCompositions.kt index 4f20b58..22db511 100644 --- a/src/main/kotlin/proofs/ConsistentCompositions.kt +++ b/src/main/kotlin/proofs/ConsistentCompositions.kt @@ -6,11 +6,15 @@ import parsing.System import java.util.* class ConsistentCompositions : Proof() { + override val kind = ProofKind.ConsistentCompositions + override fun search(component: System, ctx: ProofSearcher.IterationContext) { if (component.isLocallyConsistent.isEmpty && component is Composition) { calculateConsistency(component, ctx) + markComp(component) } else if (component.isKnownLocallyConsistent() && component is Composition) { makeChildrenConsistent(component, ctx) + markComp(component) } } diff --git a/src/main/kotlin/proofs/ConsistentRefinements.kt b/src/main/kotlin/proofs/ConsistentRefinements.kt index 209efbe..6cfcbfb 100644 --- a/src/main/kotlin/proofs/ConsistentRefinements.kt +++ b/src/main/kotlin/proofs/ConsistentRefinements.kt @@ -5,9 +5,12 @@ import parsing.System import java.util.* class ConsistentRefinements : Proof() { + override val kind = ProofKind.ConsistentRefinements + override fun search(component: System, ctx: ProofSearcher.IterationContext) { if (hasAnyRefinementRelations(component)) { makeSystemConsistent(component, ctx) + markComp(component) } } diff --git a/src/main/kotlin/proofs/ContextSwitch.kt b/src/main/kotlin/proofs/ContextSwitch.kt index 151768d..800f757 100644 --- a/src/main/kotlin/proofs/ContextSwitch.kt +++ b/src/main/kotlin/proofs/ContextSwitch.kt @@ -7,6 +7,7 @@ import parsing.Quotient import parsing.System class ContextSwitch : Proof() { + override val kind = ProofKind.ContextSwitch //override val maxContribution: Int = 4000 // A <= B and B <= A imply C[A] == C[B] (A can be replaced by B in any context) override fun search(component: System, ctx: ProofSearcher.IterationContext) { @@ -21,7 +22,10 @@ class ContextSwitch : Proof() { other.refinesThis.addAll(component.refinesThis) or other.notRefinesThis.addAll(component.notRefinesThis) - if (changed) ctx.setDirty(other, this) + if (changed) { + ctx.setDirty(other, this) + markComp(other) + } for (parent in component.parents.toList()) { replace(component, other, parent, ctx) diff --git a/src/main/kotlin/proofs/Proof.kt b/src/main/kotlin/proofs/Proof.kt index fc9fec7..172c2ad 100644 --- a/src/main/kotlin/proofs/Proof.kt +++ b/src/main/kotlin/proofs/Proof.kt @@ -5,8 +5,8 @@ import parsing.System abstract class Proof { var contribution: Int = 0 - open val maxContribution: Int = 20000 + abstract val kind: ProofKind fun reset() { contribution = 0 @@ -21,5 +21,19 @@ abstract class Proof { } } + fun markComp(component: System) { + component.relatedProofs = component.relatedProofs or kind.value + } abstract fun search(component: System, ctx: IterationContext) +} + +enum class ProofKind(val value: Int) { + ConsistentCompositions(1 shl 0), + ConsistentRefinements(1 shl 1), + ContextSwitch(1 shl 2), + QuotientRule(1 shl 3), + RefinementTransitivity(1 shl 4), + SelfRefinement(1 shl 5), + Theorem6Conj1(1 shl 6), + Theorem6Conj2(1 shl 7) } \ No newline at end of file diff --git a/src/main/kotlin/proofs/QuotientRule.kt b/src/main/kotlin/proofs/QuotientRule.kt index d160b0a..b03e8e9 100644 --- a/src/main/kotlin/proofs/QuotientRule.kt +++ b/src/main/kotlin/proofs/QuotientRule.kt @@ -5,6 +5,7 @@ import parsing.Quotient import parsing.System class QuotientRule : Proof() { + override val kind = ProofKind.QuotientRule //override val maxContribution: Int = 1000 //Quotient rule: S || T ≤ X iff? S ≤ X \\ T override fun search(component: System, ctx: ProofSearcher.IterationContext) { @@ -16,30 +17,34 @@ class QuotientRule : Proof() { val children = composition.toHashSet() children.remove(T) - val S = if (children.size==1) { + val s = if (children.size==1) { ctx.addNewComponent(children.first()) } else { ctx.addNewComponent(Composition(children)) } - S?.let{ + s?.let{ for (X in S_comp_T.thisRefines) { val X_quotient_T = ctx.addNewComponent(Quotient(X, T)) // X \\ T X_quotient_T?.let{ - if (S.refines(X_quotient_T)) { + if (s.refines(X_quotient_T)) { ctx.setDirty(X_quotient_T, this) - ctx.setDirty(S, this) + ctx.setDirty(s, this) + markComp(X_quotient_T) + markComp(s) }} } for (X in S_comp_T.thisNotRefines) { val X_quotient_T = ctx.addNewComponent(Quotient(X, T)) // X \\ T X_quotient_T?.let{ - if (S.notRefines(X_quotient_T)) { + if (s.notRefines(X_quotient_T)) { ctx.setDirty(X_quotient_T, this) - ctx.setDirty(S, this) + ctx.setDirty(s, this) + markComp(X_quotient_T) + markComp(s) }} } } diff --git a/src/main/kotlin/proofs/RefinementTransitivity.kt b/src/main/kotlin/proofs/RefinementTransitivity.kt index debe5bd..4f9b534 100644 --- a/src/main/kotlin/proofs/RefinementTransitivity.kt +++ b/src/main/kotlin/proofs/RefinementTransitivity.kt @@ -4,6 +4,8 @@ import ProofSearcher import parsing.System class RefinementTransitivity : Proof() { + override val kind = ProofKind.RefinementTransitivity + override fun search(component: System, ctx: ProofSearcher.IterationContext) { for (lhs in component.refinesThis) { if (component.inputs.containsAll(lhs.inputs) && component.outputs == lhs.outputs){ // S1 inputs ⊆ S2 inputs and S1 outputs = S2 outputs @@ -20,6 +22,8 @@ class RefinementTransitivity : Proof() { if (lhs.refines(rhs)) { ctx.setDirty(lhs, this) ctx.setDirty(rhs, this) + markComp(lhs) + markComp(rhs) } } } \ No newline at end of file diff --git a/src/main/kotlin/proofs/SelfRefinement.kt b/src/main/kotlin/proofs/SelfRefinement.kt index a89c2ff..ac75ed8 100644 --- a/src/main/kotlin/proofs/SelfRefinement.kt +++ b/src/main/kotlin/proofs/SelfRefinement.kt @@ -4,6 +4,7 @@ import ProofSearcher import parsing.System class SelfRefinement : Proof() { + override val kind = ProofKind.SelfRefinement override fun search(component: System, ctx: ProofSearcher.IterationContext) { if (hasAnyRefinementRelations(component)) { //E.g. the component is assumed to be consistent makeSelfRefining(component, ctx) @@ -13,6 +14,7 @@ class SelfRefinement : Proof() { private fun makeSelfRefining(component: System, ctx: ProofSearcher.IterationContext) { if (component.refines(component)) { ctx.setDirty(component, this) + markComp(component) } } diff --git a/src/main/kotlin/proofs/Theorem6Conj1.kt b/src/main/kotlin/proofs/Theorem6Conj1.kt index 36bde6c..365a191 100644 --- a/src/main/kotlin/proofs/Theorem6Conj1.kt +++ b/src/main/kotlin/proofs/Theorem6Conj1.kt @@ -6,6 +6,8 @@ import parsing.Conjunction import parsing.System class Theorem6Conj1 : Proof() { + override val kind = ProofKind.Theorem6Conj1 + //HSCC.Theorem6.part1, locally consistent S and T sharing the same alphabet : S ∧ T ≤ S and S ∧ T ≤ T (∧ is the same as &&) override fun search(component: System, ctx: ProofSearcher.IterationContext) { //TODO: we cant currently apply this to compositions because the ConsistentCompositions adds too many @@ -37,6 +39,7 @@ class Theorem6Conj1 : Proof() { for (child in parent.children) { if (parent.refines(child)) { ctx.setDirty(child, this) + markComp(child) } } } diff --git a/src/main/kotlin/proofs/Theorem6Conj2.kt b/src/main/kotlin/proofs/Theorem6Conj2.kt index 8880a12..aca0bee 100644 --- a/src/main/kotlin/proofs/Theorem6Conj2.kt +++ b/src/main/kotlin/proofs/Theorem6Conj2.kt @@ -5,6 +5,7 @@ import parsing.Conjunction import parsing.System class Theorem6Conj2 : Proof() { + override val kind = ProofKind.Theorem6Conj2 //HSCC.Theorem6.part2, locally consistent S, U and T sharing the same alphabet: (U <= S) and (U <= T) implies U <= (S && T) override fun search(component: System, ctx: ProofSearcher.IterationContext) { if (component.thisRefines.size > 1) { @@ -20,6 +21,8 @@ class Theorem6Conj2 : Proof() { if (component.refines(newComp)) { ctx.setDirty(newComp, this) ctx.setDirty(component, this) + markComp(newComp) + markComp(component) }} } } diff --git a/src/main/kotlin/tests/ImplicationTest.kt b/src/main/kotlin/tests/ImplicationTest.kt index 2f5baed..39a7a14 100644 --- a/src/main/kotlin/tests/ImplicationTest.kt +++ b/src/main/kotlin/tests/ImplicationTest.kt @@ -3,16 +3,16 @@ package tests import TestResult //This test acts like the implication logical operator i.e. precondition -> mainTest -class ImplicationTest(precondition: SingleTest, mainTest: SingleTest) : +class ImplicationTest(precondition: SingleTest, mainTest: SingleTest, relatedProofs: Int) : MultiTest( mainTest.testSuite, mainTest.projectPath, "(${precondition.query}) implies (${mainTest.query})", - precondition, mainTest + relatedProofs, precondition, mainTest ) { override fun toSingleTest(): SingleTest { - return SatisfiedTest(this.testSuite, this.projectPath, this.query) + return SatisfiedTest(this.testSuite, this.projectPath, this.query, this.relatedProofs) } override fun getResult(results: List): TestResult { diff --git a/src/main/kotlin/tests/NotSatisfiedTest.kt b/src/main/kotlin/tests/NotSatisfiedTest.kt index 8d770b0..a84a84a 100644 --- a/src/main/kotlin/tests/NotSatisfiedTest.kt +++ b/src/main/kotlin/tests/NotSatisfiedTest.kt @@ -2,7 +2,8 @@ package tests import TestResult -class NotSatisfiedTest(testSuite: String, projectPath: String, query: String) : SingleTest(testSuite, projectPath, query) { +class NotSatisfiedTest(testSuite: String, projectPath: String, query: String, relatedProofs: Int) + : SingleTest(testSuite, projectPath, query, relatedProofs) { override fun getResult(success: Boolean): TestResult { return TestResult(this, ResultType.from(success), ResultType.UNSATISFIED, listOf()) } diff --git a/src/main/kotlin/tests/SatisfiedTest.kt b/src/main/kotlin/tests/SatisfiedTest.kt index 46e5677..718a0e2 100644 --- a/src/main/kotlin/tests/SatisfiedTest.kt +++ b/src/main/kotlin/tests/SatisfiedTest.kt @@ -2,7 +2,8 @@ package tests import TestResult -class SatisfiedTest(testSuite: String, projectPath: String, query: String) : SingleTest(testSuite, projectPath, query) { +class SatisfiedTest(testSuite: String, projectPath: String, query: String, relatedProofs: Int) + : SingleTest(testSuite, projectPath, query, relatedProofs) { override fun getResult(success: Boolean): TestResult { return TestResult(this, ResultType.from(success), ResultType.SATISFIED, listOf()) } diff --git a/src/main/kotlin/tests/Test.kt b/src/main/kotlin/tests/Test.kt index 98d5030..6be4b9f 100644 --- a/src/main/kotlin/tests/Test.kt +++ b/src/main/kotlin/tests/Test.kt @@ -2,7 +2,7 @@ package tests import TestResult -abstract class Test(val testSuite: String, val projectPath: String) { +abstract class Test(val testSuite: String, val projectPath: String, val relatedProofs: Int) { val type = this.javaClass.simpleName abstract fun queries(): List abstract fun toSingleTest(): SingleTest @@ -17,7 +17,8 @@ abstract class Test(val testSuite: String, val projectPath: String) { } } -open class SingleTest(testSuite: String, projectPath: String, val query: String) : Test(testSuite, projectPath) { +open class SingleTest(testSuite: String, projectPath: String, val query: String, relatedProofs: Int) + : Test(testSuite, projectPath, relatedProofs) { open fun getResult(success: Boolean): TestResult { throw error("Unimplemented")} override fun queries(): List { return listOf(query) @@ -28,7 +29,8 @@ open class SingleTest(testSuite: String, projectPath: String, val query: String) } } -abstract class MultiTest(testSuite: String, projectPath: String, val query: String, vararg val tests: Test) : Test(testSuite, projectPath) { +abstract class MultiTest(testSuite: String, projectPath: String, val query: String, relatedProofs: Int, vararg val tests: Test) + : Test(testSuite, projectPath, relatedProofs) { abstract fun getResult(results: List) : TestResult override fun queries(): List { return tests.flatMap { it.queries() } diff --git a/src/main/kotlin/tests/testgeneration/ConjunctionCommutativeTests.kt b/src/main/kotlin/tests/testgeneration/ConjunctionCommutativeTests.kt index caf5ceb..f28afc2 100644 --- a/src/main/kotlin/tests/testgeneration/ConjunctionCommutativeTests.kt +++ b/src/main/kotlin/tests/testgeneration/ConjunctionCommutativeTests.kt @@ -51,7 +51,8 @@ class ConjunctionCommutativeTests : TestRule { return SatisfiedTest( "ConjCommutativeRefinement", original.getProjectFolder(), - "refinement: ${if (flip) first else second} <= ${if (flip) second else first}" + "refinement: ${if (flip) first else second} <= ${if (flip) second else first}", + original.relatedProofs ) } } \ No newline at end of file diff --git a/src/main/kotlin/tests/testgeneration/ConjunctionIdentityTests.kt b/src/main/kotlin/tests/testgeneration/ConjunctionIdentityTests.kt index 03b6eaf..5ccc860 100644 --- a/src/main/kotlin/tests/testgeneration/ConjunctionIdentityTests.kt +++ b/src/main/kotlin/tests/testgeneration/ConjunctionIdentityTests.kt @@ -32,12 +32,14 @@ class ConjunctionIdentityTests : TestRule { return ImplicationTest(SatisfiedTest( "ConjIdentityRefinement::Precondition", system.getProjectFolder(), - "consistency: $first" + "consistency: $first", + system.relatedProofs ), SatisfiedTest( "ConjIdentityRefinement", system.getProjectFolder(), - "refinement: ${if (flip) first else second} <= ${if (flip) second else first}" - )) + "refinement: ${if (flip) first else second} <= ${if (flip) second else first}", + system.relatedProofs or other.relatedProofs + ), system.relatedProofs or other.relatedProofs) } diff --git a/src/main/kotlin/tests/testgeneration/ConsistencyTests.kt b/src/main/kotlin/tests/testgeneration/ConsistencyTests.kt index 69599be..30c2e7e 100644 --- a/src/main/kotlin/tests/testgeneration/ConsistencyTests.kt +++ b/src/main/kotlin/tests/testgeneration/ConsistencyTests.kt @@ -29,13 +29,15 @@ class ConsistencyTests : TestRule { SatisfiedTest( "Consistency", system.getProjectFolder(), - "consistency: ${system.getName()}" + "consistency: ${system.getName()}", + system.relatedProofs ) private fun createNonConsistencyTest(system: System) = NotSatisfiedTest( "NonConsistency", system.getProjectFolder(), - "consistency: ${system.getName()}" + "consistency: ${system.getName()}", + system.relatedProofs ) } \ No newline at end of file diff --git a/src/main/kotlin/tests/testgeneration/ImpliedRefinementTest.kt b/src/main/kotlin/tests/testgeneration/ImpliedRefinementTest.kt index 3ef79d6..d5e25b5 100644 --- a/src/main/kotlin/tests/testgeneration/ImpliedRefinementTest.kt +++ b/src/main/kotlin/tests/testgeneration/ImpliedRefinementTest.kt @@ -34,35 +34,38 @@ class ImpliedRefinementTest: TestRule { val precondition = createPreconditionTest(system) val mainTest = createSelfRefinementTest(system) - return ImplicationTest(precondition, mainTest) + return ImplicationTest(precondition, mainTest, system.relatedProofs) } private fun createTest(lhs: System, rhs: System, preconditionSystem: System): Test { val precondition = createPreconditionTest(preconditionSystem) val mainTest = createRefinementTest(lhs, rhs) - return ImplicationTest(precondition, mainTest) + return ImplicationTest(precondition, mainTest, mainTest.relatedProofs) } private fun createPreconditionTest(system: System) = SatisfiedTest( "ImpliedRefinement::Precondition", system.getProjectFolder(), - "consistency: ${system.getName()}" + "consistency: ${system.getName()}", + system.relatedProofs ) private fun createSelfRefinementTest(system: System) = SatisfiedTest( "ImpliedSelfRefinement", system.getProjectFolder(), - "refinement: ${system.getName()} <= ${system.getName()}" + "refinement: ${system.getName()} <= ${system.getName()}", + system.relatedProofs ) private fun createRefinementTest(lhs: System, rhs: System) = SatisfiedTest( "ImpliedRefinement", lhs.getProjectFolder(), - "refinement: ${lhs.getName()} <= ${rhs.getName()}" + "refinement: ${lhs.getName()} <= ${rhs.getName()}", + lhs.relatedProofs or rhs.relatedProofs ) diff --git a/src/main/kotlin/tests/testgeneration/NotRefinement.kt b/src/main/kotlin/tests/testgeneration/NotRefinement.kt index c4f4e8f..a11088b 100644 --- a/src/main/kotlin/tests/testgeneration/NotRefinement.kt +++ b/src/main/kotlin/tests/testgeneration/NotRefinement.kt @@ -23,6 +23,7 @@ class NotRefinement : TestRule { NotSatisfiedTest( "NotRefines", system.getProjectFolder(), - "refinement: ${system.getName()} <= ${other.getName()}" + "refinement: ${system.getName()} <= ${other.getName()}", + system.relatedProofs ) } \ No newline at end of file diff --git a/src/main/kotlin/tests/testgeneration/RefinementTests.kt b/src/main/kotlin/tests/testgeneration/RefinementTests.kt index 617954f..6c639dd 100644 --- a/src/main/kotlin/tests/testgeneration/RefinementTests.kt +++ b/src/main/kotlin/tests/testgeneration/RefinementTests.kt @@ -34,14 +34,16 @@ class RefinementTests : TestRule { SatisfiedTest( "Refinement", system.getProjectFolder(), - "refinement: ${system.getName()} <= ${other.getName()}" + "refinement: ${system.getName()} <= ${other.getName()}", + system.relatedProofs or other.relatedProofs ) private fun createSelfRefinementTest(system: System) = SatisfiedTest( "SelfRefinement", system.getProjectFolder(), - "refinement: ${system.getName()} <= ${system.getName()}" + "refinement: ${system.getName()} <= ${system.getName()}", + system.relatedProofs ) } \ No newline at end of file From 7a4dacd1d224aba5984e864ec13ccb641282f4a8 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Tue, 29 Nov 2022 15:42:38 +0100 Subject: [PATCH 3/3] Remove log file --- logs.txt | 96 -------------------------------------------------------- 1 file changed, 96 deletions(-) delete mode 100644 logs.txt diff --git a/logs.txt b/logs.txt deleted file mode 100644 index 05f66d3..0000000 --- a/logs.txt +++ /dev/null @@ -1,96 +0,0 @@ -Tests generated for engine 'Reveaal' on 29/11/2022 03:18:43 ------------------------------------------------------------ - -samples/json/EcdarUniversity - ImplicationTest: ImpliedRefinement - "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((Adm2 && HalfAdm1) || Researcher) && ((Adm2 && HalfAdm2) || Researcher) && (Adm2 || Researcher)) \\ Adm2)" - "refinement: Researcher <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((Adm2 && HalfAdm1) || Researcher) && ((Adm2 && HalfAdm2) || Researcher) && (Adm2 || Researcher)) \\ Adm2)" - ImplicationTest: ImpliedSelfRefinement - "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2))" - "refinement: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2)) <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2))" - ImplicationTest: ImpliedRefinement - "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Researcher)" - "refinement: Machine <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Researcher)" - ImplicationTest: ImpliedSelfRefinement - "consistency: (((Administration || Machine || Researcher) \\ Administration) \\ Researcher)" - "refinement: (((Administration || Machine || Researcher) \\ Administration) \\ Researcher) <= (((Administration || Machine || Researcher) \\ Administration) \\ Researcher)" - ImplicationTest: ImpliedSelfRefinement - "consistency: (((HalfAdm1 && HalfAdm2) || Researcher) \\ (Adm2 && HalfAdm2))" - "refinement: (((HalfAdm1 && HalfAdm2) || Researcher) \\ (Adm2 && HalfAdm2)) <= (((HalfAdm1 && HalfAdm2) || Researcher) \\ (Adm2 && HalfAdm2))" - ImplicationTest: ImpliedSelfRefinement - "consistency: (((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) \\ Adm2)" - "refinement: (((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) \\ Adm2) <= (((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) \\ Adm2)" - ImplicationTest: ImpliedSelfRefinement - "consistency: (((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm1) || Machine))" - "refinement: (((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm1) || Machine)) <= (((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm1) || Machine))" - ImplicationTest: ImpliedRefinement - "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ (Adm2 && HalfAdm1))" - "refinement: Researcher <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ (Adm2 && HalfAdm1))" - ImplicationTest: ImpliedSelfRefinement - "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ (Adm2 && HalfAdm1))" - "refinement: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ (Adm2 && HalfAdm1)) <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ (Adm2 && HalfAdm1))" - ImplicationTest: ImpliedRefinement - "consistency: (((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((Adm2 && HalfAdm1) || Researcher))" - "refinement: ((HalfAdm1 && HalfAdm2) || Researcher) <= (((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((Adm2 && HalfAdm1) || Researcher))" - ImplicationTest: ImpliedRefinement - "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((HalfAdm1 && HalfAdm2) || Researcher) && (Adm2 || Researcher)) \\ (Adm2 && HalfAdm2))" - "refinement: Researcher <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Researcher) && ((HalfAdm1 && HalfAdm2) || Researcher) && (Adm2 || Researcher)) \\ (Adm2 && HalfAdm2))" - ImplicationTest: ImpliedSelfRefinement - "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Machine)" - "refinement: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Machine) <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1 && HalfAdm2)) \\ Machine)" - ImplicationTest: ImpliedSelfRefinement - "consistency: ((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Adm2)" - "refinement: ((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Adm2) <= ((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Adm2)" - ImplicationTest: ImpliedRefinement - "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ Researcher)" - "refinement: (HalfAdm1 && HalfAdm2) <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ Researcher)" - NotSatisfiedTest: NotRefines - "refinement: Researcher <= ((Spec \\ Machine) \\ (Adm2 && HalfAdm1 && HalfAdm2))" - ImplicationTest: ImpliedRefinement - "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2))" - "refinement: (Machine || Researcher) <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2))" - ImplicationTest: ImpliedRefinement - "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher)) \\ (HalfAdm1 && HalfAdm2))" - "refinement: (Machine || Researcher) <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher)) \\ (HalfAdm1 && HalfAdm2))" - ImplicationTest: ImpliedRefinement - "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1))" - "refinement: Machine <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1))" - ImplicationTest: ImpliedRefinement - "consistency: ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm2) || Machine) && ((HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ Adm2)" - "refinement: Machine <= ((((Adm2 && HalfAdm1 && HalfAdm2) || Machine) && ((Adm2 && HalfAdm2) || Machine) && ((HalfAdm1 && HalfAdm2) || Machine) && (Adm2 || Machine)) \\ Adm2)" - ImplicationTest: ImpliedRefinement - "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Machine) \\ (HalfAdm1 && HalfAdm2))" - "refinement: Researcher <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Machine) \\ (HalfAdm1 && HalfAdm2))" - ImplicationTest: ImpliedRefinement - "consistency: (Adm2 && HalfAdm1 && HalfAdm2)" - "refinement: (HalfAdm1 && HalfAdm2) <= (Adm2 && HalfAdm1 && HalfAdm2)" - ImplicationTest: ImpliedSelfRefinement - "consistency: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2)) \\ Researcher)" - "refinement: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2)) \\ Researcher) <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm2)) \\ Researcher)" - ImplicationTest: ImpliedRefinement - "consistency: (((((Adm2 && HalfAdm1) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1)) \\ Machine)" - "refinement: Researcher <= (((((Adm2 && HalfAdm1) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ (Adm2 && HalfAdm1)) \\ Machine)" - ImplicationTest: ImpliedRefinement - "consistency: (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ (Adm2 && HalfAdm1 && HalfAdm2))" - "refinement: Researcher <= (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher)) \\ Machine) \\ (Adm2 && HalfAdm1 && HalfAdm2))" - ImplicationTest: ImpliedSelfRefinement - "consistency: (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2))" - "refinement: (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2)) <= (((((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) \\ Researcher) \\ (Adm2 && HalfAdm1 && HalfAdm2))" - -samples/xml/delayRefinement.xml - ImplicationTest: ImpliedRefinement - "consistency: (K5 && Z2)" - "refinement: (K5 && Z2) <= K5" - SatisfiedTest: Consistency - "consistency: (F1 || F2)" - ImplicationTest: ImpliedRefinement - "consistency: (K4 && P0)" - "refinement: (K4 && P0) <= K4" - ImplicationTest: ImpliedRefinement - "consistency: (L4 && P6)" - "refinement: (L4 && P6) <= L4" - -samples/json/Conjunction - SatisfiedTest: SelfRefinement - "refinement: Test4 <= Test4" -