Skip to content

Commit

Permalink
Add tests for kore-rpc terminal and cut-point rules (runtimeverific…
Browse files Browse the repository at this point in the history
…ation/pyk#48)

~Blocked on: #2974
Fixes #41

Co-authored-by: devops <devops@runtimeverification.com>
  • Loading branch information
2 people authored and Baltoli committed Apr 9, 2024
1 parent 978c2de commit d662565
Show file tree
Hide file tree
Showing 5 changed files with 19 additions and 4 deletions.
3 changes: 2 additions & 1 deletion pyk/Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@ FROM runtimeverificationinc/kframework-k:ubuntu-${K_DISTRO}-${K_VERSION}

RUN apt-get update \
&& apt-get install -y \
curl
curl \
graphviz

RUN curl -sSL https://install.python-poetry.org | POETRY_HOME=/usr python3 - \
&& poetry --version
Expand Down
2 changes: 1 addition & 1 deletion pyk/deps/K_VERSION
Original file line number Diff line number Diff line change
@@ -1 +1 @@
5.3.195
5.4.13
2 changes: 1 addition & 1 deletion pyk/package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.32
0.1.33
2 changes: 1 addition & 1 deletion pyk/pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "pyk"
version = "0.1.32"
version = "0.1.33"
description = ""
authors = [
"Runtime Verification, Inc. <contact@runtimeverification.com>",
Expand Down
14 changes: 14 additions & 0 deletions pyk/src/integration_tests/kore/test_kore_client.py
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,14 @@
from pyk.kore.parser import KoreParser
from pyk.kore.rpc import (
BranchingResult,
CutPointResult,
DepthBoundResult,
ExecuteResult,
ImpliesResult,
KoreClientError,
State,
StuckResult,
TerminalResult,
)
from pyk.kore.syntax import DV, Equals, EVar, Implies, Pattern, SortApp, SortVar, String, Top

Expand Down Expand Up @@ -52,6 +54,18 @@ def test_execute(self) -> None:
('branching', 0, {}, BranchingResult(state=state(2), depth=2, next_states=(state(4), state(3)))),
('depth-bound', 0, {'max_depth': 2}, DepthBoundResult(state=state(2), depth=2)),
('stuck', 4, {}, StuckResult(state=state(6), depth=2)),
(
'cut-point',
4,
{'cut_point_rules': ['KORE-RPC-TEST.r56']},
CutPointResult(state=state(5), depth=1, next_states=(state(6),), rule='KORE-RPC-TEST.r56'),
),
(
'terminal',
4,
{'terminal_rules': ['KORE-RPC-TEST.r56']},
TerminalResult(state=state(6), depth=2, rule='KORE-RPC-TEST.r56'),
),
)

for test_name, n, params, expected in test_data:
Expand Down

0 comments on commit d662565

Please sign in to comment.