Reorganize tests

runtimeverification · Aug 21, 2024 · 09d68bb · 09d68bb
1 parent e155e58
commit 09d68bb
Show file tree

Hide file tree

Showing 5 changed files with 225 additions and 202 deletions.
diff --git 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  `<k>b</k><int>N</int> \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
diff --git a/booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.booster-dev b/booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.booster-dev
@@ -0,0 +1,215 @@
+{
+    "jsonrpc": "2.0",
+    "id": 1,
+    "result": {
+        "reason": "stuck",
+        "depth": 0,
+        "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": "d"
+                                                }
+                                            ]
+                                        },
+                                        {
+                                            "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"
+                                }
+                            ]
+                        }
+                    ]
+                }
+            },
+            "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": "N",
+                                        "sort": {
+                                            "tag": "SortApp",
+                                            "name": "SortInt",
+                                            "args": []
+                                        }
+                                    },
+                                    {
+                                        "tag": "DV",
+                                        "sort": {
+                                            "tag": "SortApp",
+                                            "name": "SortInt",
+                                            "args": []
+                                        },
+                                        "value": "0"
+                                    }
+                                ]
+                            }
+                        },
+                        {
+                            "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": "LblnotBool'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"
+                                            }
+                                        ]
+                                    }
+                                ]
+                            }
+                        }
+                    ]
+                }
+            }
+        }
+    }
+}
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