From 2ad1c793af7f155db16218185771163958fffc69 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 21 Aug 2024 14:54:48 +0200 Subject: [PATCH] Reorganize tests --- .../rpc-integration/test-vacuous/README.md | 10 + .../params-vacuous-but-rewritten.json | 1 - .../state-vacuous-but-rewritten.execute | 1 - .../state-vacuous-not-rewritten.execute | 200 ------------------ 4 files changed, 10 insertions(+), 202 deletions(-) delete mode 100644 booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json delete mode 120000 booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute delete mode 100644 booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute diff --git a/booster/test/rpc-integration/test-vacuous/README.md b/booster/test/rpc-integration/test-vacuous/README.md index bd26765c7c7..282675ad7da 100644 --- a/booster/test/rpc-integration/test-vacuous/README.md +++ b/booster/test/rpc-integration/test-vacuous/README.md @@ -47,5 +47,15 @@ Rules `init` and `AC` introduce constraints on this variable: _Expected:_ - The state is simplified and discovered to be `vacuous` (with state `b`). +1) _unchecked-vacuous-rewritten_ + + _Input:_ same as _vacuous-not-rewritten_ + - `execute` request with initial state `bN \and N + ==Int 1 \and N =/=Int 1` (A contradiction in the initial constraints). + + _Expected:_ + - the input constraints are not checked for satisfiability (`"assume-defined": true` is in params) + - one rewrite step is made and the result is `stuck` + With `kore-rpc-dev`, some contradictions will be discovered before or while attempting to rewrite (at the time of writing, it returns `stuck`, though). diff --git a/booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json b/booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json deleted file mode 100644 index c58212fd427..00000000000 --- a/booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json +++ /dev/null @@ -1 +0,0 @@ -{ "assume-defined": true } diff --git a/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute b/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute deleted file mode 120000 index bc6397970f8..00000000000 --- a/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute +++ /dev/null @@ -1 +0,0 @@ -state-vacuous-not-rewritten.execute \ No newline at end of file diff --git a/booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute b/booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute deleted file mode 100644 index 0dc921acb08..00000000000 --- a/booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute +++ /dev/null @@ -1,200 +0,0 @@ -{ - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "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": "b" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "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" - } - ] - } - ] - }, - "second": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "Equals", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "first": { - "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" - } - ] - }, - "second": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - } - }, - "second": { - "tag": "Equals", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "first": { - "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - }, - "second": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - } - } - } - } -}