diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden index e7d03842a4d..dabde089fdb 100644 --- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden +++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden @@ -1,6 +1,7 @@ {"context":["proxy"],"message":"Loading definition from resources/log-simplify-json.kore, main module \"IMP-VERIFICATION\""} {"context":["proxy"],"message":"Starting RPC server"} {"context":["proxy"],"message":"Processing request 4"} +{"context":[{"request":"4"},"booster","execute",{"term":"bd7c50d"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\"))"} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} @@ -51,7 +52,6 @@ {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"fd81940"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"50120f3"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} -{"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} diff --git a/booster/test/rpc-integration/test-substitutions/README.md b/booster/test/rpc-integration/test-substitutions/README.md index 1c7a208f588..23112025662 100644 --- a/booster/test/rpc-integration/test-substitutions/README.md +++ b/booster/test/rpc-integration/test-substitutions/README.md @@ -31,10 +31,9 @@ NB: Booster applies the given substitution before performing any action. - with an additional constraint `Y = 1 +Int X` (internalised as a substitution) - leading to a contradictory constraint `X = 1 +Int X` after rewriting and adding `Y =Int X` from the `ensures`-clause - - `kore-rpc-booster` returns `vacuous` after 1 step - - `kore-rpc-dev` returns `vacuous` after 0 steps (detects the contradiction earlier) - - `kore-rpc-dev` reproduces the exact input as `state` while - `kore-rpc-booster` splits off `substitution` (from input) and `predicate` (from the rule) + - `kore-rpc-booster` and `booster-dev` return `vacuous` after 0 step, substitution `Y` for `X +Int 1` in the state. However, `kore-rpc-booster` and `booster-dev` disagree a little on the value in the substitution, hence the two responses. + - `kore-rpc-dev` returns `vacuous` after 0 steps and reproduces the exact input as `state` + * `state-circular-equations.execute` - starts from `concrete-subst` - with two equations that have circular dependencies: `Y = 1 +Int X`, `X = Y -Int 1` @@ -42,6 +41,6 @@ NB: Booster applies the given substitution before performing any action. * `state-symbolic-bottom-predicate.execute` - starts from `symbolic-subst` - with an equation that is instantly false: `X = 1 +Int X` - - leading to a vacuous state in `kore-rpc-booster` after rewriting once, + - leading to a vacuous state in `booster-dev` and `kore-rpc-booster`, - while `kore-rpc-dev` returns `stuck` instantly after 0 steps, returning the exact input as `state`. diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev index b0121481903..259a441aeb9 100644 --- a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev @@ -225,61 +225,13 @@ } }, { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - }, - { - "tag": "App", - "name": "Lbl'Unds'-Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - } - ] + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } } ] } diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev deleted file mode 100644 index 9aec4d52896..00000000000 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev +++ /dev/null @@ -1,240 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 1, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "a" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'jnt'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - } - ] - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json index be972500f9c..8196839aaad 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json @@ -3,7 +3,7 @@ "id": 1, "result": { "reason": "vacuous", - "depth": 1, + "depth": 0, "state": { "term": { "format": "KORE", @@ -46,7 +46,7 @@ "name": "SortState", "args": [] }, - "value": "a" + "value": "symbolic-subst" } ] }, @@ -115,114 +115,57 @@ "format": "KORE", "version": 1, "term": { - "tag": "And", + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - } - ] - } + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, - "second": { + { "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "name": "Lbl'UndsPlus'Int'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" }, { "tag": "EVar", - "name": "Y", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", @@ -231,8 +174,8 @@ } ] } - } - ] + ] + } } } } diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-two-substitutions.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-two-substitutions.booster-dev index 40c6e95a249..58a6ab33aaa 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-two-substitutions.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-two-substitutions.booster-dev @@ -87,22 +87,22 @@ "sorts": [], "args": [ { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "1" + } }, { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" } ] } diff --git a/booster/test/rpc-integration/test-vacuous/README.md b/booster/test/rpc-integration/test-vacuous/README.md index 00c6823dc40..9464e3a6de8 100644 --- a/booster/test/rpc-integration/test-vacuous/README.md +++ b/booster/test/rpc-integration/test-vacuous/README.md @@ -38,7 +38,7 @@ Rules `init` and `AC` introduce constraints on this variable: _Expected:_ - The rewrite is stuck with `dN \and...(contradiction)` - The result is simplified and discovered to be `vacuous` (with state `d`). -1) _vacuous-but-rewritten_ +1) _vacuous-not-rewritten_ _Input:_ - `execute` request with initial state `bN \and N diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-not-rewritten.json similarity index 84% rename from booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json rename to booster/test/rpc-integration/test-vacuous/response-vacuous-not-rewritten.json index b7cf3878338..3d880fa432c 100644 --- a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json +++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-not-rewritten.json @@ -3,7 +3,7 @@ "id": 1, "result": { "reason": "vacuous", - "depth": 1, + "depth": 0, "state": { "term": { "format": "KORE", @@ -46,7 +46,7 @@ "name": "SortState", "args": [] }, - "value": "d" + "value": "b" } ] }, @@ -129,7 +129,7 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", "sorts": [], "args": [ { @@ -176,33 +176,26 @@ }, "second": { "tag": "App", - "name": "LblnotBool'Unds'", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", "sorts": [], "args": [ { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" } ] } diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.kore-rpc-dev b/booster/test/rpc-integration/test-vacuous/response-vacuous-not-rewritten.kore-rpc-dev similarity index 100% rename from booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.kore-rpc-dev rename to booster/test/rpc-integration/test-vacuous/response-vacuous-not-rewritten.kore-rpc-dev diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json index d3b14044a81..9d4198621d8 100644 --- a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json +++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json @@ -129,7 +129,7 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", "sorts": [], "args": [ { @@ -176,33 +176,26 @@ }, "second": { "tag": "App", - "name": "LblnotBool'Unds'", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", "sorts": [], "args": [ { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" } ] } diff --git a/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute b/booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute similarity index 100% rename from booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute rename to booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute diff --git a/scripts/booster-integration-tests.sh b/scripts/booster-integration-tests.sh index 3a24d3db647..bde164c1954 100755 --- a/scripts/booster-integration-tests.sh +++ b/scripts/booster-integration-tests.sh @@ -28,12 +28,12 @@ for dir in $(ls -d test-*); do name=${dir##test-} echo "Running $name..." case "$name" in - "a-to-f" | "diamond") + "a-to-f" | "diamond" | "substitutions") SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;; - "substitutions" | "vacuous" | "pathological-add-module") + "vacuous" | "pathological-add-module") SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;;