From b3a5138b2ebbb0bd10f7725ec94ff64bd2caead0 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 28 Feb 2022 19:11:28 +0100
Subject: [PATCH] Use new getters for properties/invariant/assertions in :check
---
CHANGELOG.md | 1 +
build.gradle | 2 +-
notebooks/tests/check.ipynb | 222 ++++++++++++++++++
.../prob2/jupyter/commands/CheckCommand.java | 70 +++---
4 files changed, 259 insertions(+), 36 deletions(-)
create mode 100644 notebooks/tests/check.ipynb
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1d415eb..b8922b2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,7 @@
## [(next version)](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.3.1-SNAPSHOT-all.jar?job=test)
+* Updated ProB 2 to version 4.0.0-SNAPSHOT.
* Disabled LaTeX formatting inside `:check` tables as well, because of the layout issues mentioned below.
## [1.3.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar)
diff --git a/build.gradle b/build.gradle
index 11c6368..3ddc233 100644
--- a/build.gradle
+++ b/build.gradle
@@ -39,7 +39,7 @@ dependencies {
implementation(group: "ch.qos.logback", name: "logback-classic", version: "1.2.10")
implementation(group: "com.google.code.gson", name: "gson", version: "2.8.9")
implementation(group: "com.google.guava", name: "guava", version: "31.0.1-jre")
- implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "3.15.0")
+ implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "4.0.0-SNAPSHOT")
implementation(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.3.0")
implementation(group: "org.jetbrains", name: "annotations", version: "23.0.0")
implementation(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")
diff --git a/notebooks/tests/check.ipynb b/notebooks/tests/check.ipynb
new file mode 100644
index 0000000..d8a288f
--- /dev/null
+++ b/notebooks/tests/check.ipynb
@@ -0,0 +1,222 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "36c2fbc3",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "```\n",
+ ":check WHAT\n",
+ "```\n",
+ "\n",
+ "Check the machine's properties, invariant, or assertions in the current state.\n",
+ "\n",
+ "The properties/invariant/assertions are checked and displayed in table form. Each row corresponds to a part of the properties/invariant conjunction, or to an assertion."
+ ],
+ "text/plain": [
+ ":check WHAT\n",
+ "Check the machine's properties, invariant, or assertions in the current state.\n",
+ "\n",
+ "The properties/invariant/assertions are checked and displayed in table form. Each row corresponds to a part of the properties/invariant conjunction, or to an assertion."
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help :check"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "69f51548",
+ "metadata": {},
+ "source": [
+ "`:check` works for classical B machines."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "daa741b3",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: CheckTest"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE CheckTest\n",
+ "CONSTANTS x, y\n",
+ "PROPERTIES x : {1, 2} & y : {3, 4}\n",
+ "VARIABLES a, b\n",
+ "INVARIANT a : 0..x & b : 1..y\n",
+ "INITIALISATION a := x; b := y\n",
+ "ASSERTIONS a <= x; b <= y\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "0f0f8bc9",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: SETUP_CONSTANTS()"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "ca180263",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "a4901fab",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|Predicate|Value|\n",
+ "|---|---|\n",
+ "|x∈{1,2}|TRUE|\n",
+ "|y∈{3,4}|TRUE|"
+ ],
+ "text/plain": [
+ "x:{1,2} = TRUE\n",
+ "y:{3,4} = TRUE"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":check properties"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "62fe69ce",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|Predicate|Value|\n",
+ "|---|---|\n",
+ "|a∈0‥x|TRUE|\n",
+ "|b∈1‥y|TRUE|"
+ ],
+ "text/plain": [
+ "a:0..x = TRUE\n",
+ "b:1..y = TRUE"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":check invariant"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "d2054303",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|Predicate|Value|\n",
+ "|---|---|\n",
+ "|a≤x|TRUE|\n",
+ "|b≤y|TRUE|"
+ ],
+ "text/plain": [
+ "a<=x = TRUE\n",
+ "b<=y = TRUE"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":check assertions"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "72e11ab6",
+ "metadata": {},
+ "source": [
+ "TODO: Test for Event-B"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
index 8fd4fd5..db72f85 100644
--- a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
@@ -1,22 +1,20 @@
package de.prob2.jupyter.commands;
-import java.util.ArrayList;
import java.util.Collections;
-import java.util.HashMap;
import java.util.List;
-import java.util.Map;
import java.util.StringJoiner;
import java.util.stream.Collectors;
+import java.util.stream.Stream;
import com.google.inject.Inject;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.IEvalElement;
-import de.prob.model.classicalb.Assertion;
+import de.prob.model.classicalb.ClassicalBMachine;
+import de.prob.model.representation.AbstractElement;
import de.prob.model.representation.AbstractFormulaElement;
-import de.prob.model.representation.AbstractTheoremElement;
-import de.prob.model.representation.Axiom;
-import de.prob.model.representation.Invariant;
+import de.prob.model.representation.ConstantsComponent;
+import de.prob.model.representation.Machine;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.unicode.UnicodeTranslator;
@@ -37,15 +35,6 @@ import org.jetbrains.annotations.NotNull;
public final class CheckCommand implements Command {
private static final @NotNull Parameter.RequiredSingle WHAT_PARAM = Parameter.required("what");
- private static final @NotNull Map<@NotNull String, @NotNull Class<? extends AbstractTheoremElement>> CHILDREN_BASE_CLASS_MAP;
- static {
- final Map<String, Class<? extends AbstractTheoremElement>> childrenBaseClassMap = new HashMap<>();
- childrenBaseClassMap.put("properties", Axiom.class);
- childrenBaseClassMap.put("invariant", Invariant.class);
- childrenBaseClassMap.put("assertions", Assertion.class);
- CHILDREN_BASE_CLASS_MAP = Collections.unmodifiableMap(childrenBaseClassMap);
- }
-
private final @NotNull AnimationSelector animationSelector;
@Inject
@@ -83,27 +72,39 @@ public final class CheckCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final String what = args.get(WHAT_PARAM);
- if (!CHILDREN_BASE_CLASS_MAP.containsKey(what)) {
- throw new UserErrorException("Don't know how to check " + what);
- }
- final Class<? extends AbstractTheoremElement> childrenBaseClass = CHILDREN_BASE_CLASS_MAP.get(what);
final Trace trace = this.animationSelector.getCurrentTrace();
- // Find all children of a subclass of childrenBaseClass.
- // This needs to be done manually, because getChildrenOfType only returns children whose class *exactly* matches the given class.
- // For example, getChildrenOfType(Axiom.class) doesn't return children of class Property (which is a subclass of Axiom).
- final List<IEvalElement> formulas = new ArrayList<>();
- trace.getStateSpace().getMainComponent().getChildren().forEach((clazz, children) -> {
- if (childrenBaseClass.isAssignableFrom(clazz)) {
- children.stream()
- .map(childrenBaseClass::cast)
- .map(AbstractFormulaElement::getFormula)
- .collect(Collectors.toCollection(() -> formulas));
- }
- });
+ final AbstractElement mainComponent = trace.getStateSpace().getMainComponent();
+ final List<? extends AbstractFormulaElement> elements;
+ switch (what) {
+ case "properties":
+ if (!(mainComponent instanceof ConstantsComponent)) {
+ throw new UserErrorException("Checking " + what + " is only supported for classical B machines or Event-B contexts");
+ }
+ elements = ((ConstantsComponent)mainComponent).getAxioms();
+ break;
+
+ case "invariant":
+ if (!(mainComponent instanceof Machine)) {
+ throw new UserErrorException("Checking " + what + " is only supported for classical B or Event-B machines");
+ }
+ elements = ((Machine)mainComponent).getInvariants();
+ break;
+
+ case "assertions":
+ if (!(mainComponent instanceof ClassicalBMachine)) {
+ throw new UserErrorException("Checking " + what + " is only supported for classical B machines");
+ }
+ elements = ((ClassicalBMachine)mainComponent).getAssertions();
+ break;
+
+ default:
+ throw new UserErrorException("Don't know how to check " + what);
+ }
final StringJoiner sjPlain = new StringJoiner("\n");
final StringJoiner sjMarkdown = new StringJoiner("\n", "|Predicate|Value|\n|---|---|\n", "");
- for (final IEvalElement f : formulas) {
+ for (final AbstractFormulaElement element : elements) {
+ final IEvalElement f = element.getFormula();
final AbstractEvalResult result = trace.evalCurrent(f);
sjPlain.add(f.getCode() + " = " + CommandUtils.inlinePlainTextForEvalResult(result));
sjMarkdown.add("|" + UnicodeTranslator.toUnicode(f.getCode()) + "|" + CommandUtils.inlineMarkdownForEvalResult(result) + '|');
@@ -123,8 +124,7 @@ public final class CheckCommand implements Command {
return new ParameterCompleters(Collections.singletonMap(
WHAT_PARAM, (argString, at) -> {
final String prefix = argString.substring(0, at);
- return new ReplacementOptions(CHILDREN_BASE_CLASS_MAP.keySet()
- .stream()
+ return new ReplacementOptions(Stream.of("properties", "invariant", "assertions")
.filter(s -> s.startsWith(prefix))
.collect(Collectors.toList()), 0, argString.length());
}
--
GitLab