Commit b3a5138b authored by dgelessus's avatar dgelessus
Browse files

Use new getters for properties/invariant/assertions in :check

parent 8b2e511d
Pipeline #82071 passed with stage
in 2 minutes and 2 seconds
......@@ -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)
......
......@@ -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")
......
{
"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
}
%% Cell type:code id:36c2fbc3 tags:
``` prob
:help :check
```
%%%% Output: execute_result
```
:check WHAT
```
Check the machine's properties, invariant, or assertions in the current state.
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.
:check WHAT
Check the machine's properties, invariant, or assertions in the current state.
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.
%% Cell type:markdown id:69f51548 tags:
`:check` works for classical B machines.
%% Cell type:code id:daa741b3 tags:
``` prob
MACHINE CheckTest
CONSTANTS x, y
PROPERTIES x : {1, 2} & y : {3, 4}
VARIABLES a, b
INVARIANT a : 0..x & b : 1..y
INITIALISATION a := x; b := y
ASSERTIONS a <= x; b <= y
END
```
%%%% Output: execute_result
Loaded machine: CheckTest
%% Cell type:code id:0f0f8bc9 tags:
``` prob
:constants
```
%%%% Output: execute_result
Executed operation: SETUP_CONSTANTS()
%% Cell type:code id:ca180263 tags:
``` prob
:init
```
%%%% Output: execute_result
Executed operation: INITIALISATION()
%% Cell type:code id:a4901fab tags:
``` prob
:check properties
```
%%%% Output: execute_result
|Predicate|Value|
|---|---|
|x∈{1,2}|TRUE|
|y∈{3,4}|TRUE|
x:{1,2} = TRUE
y:{3,4} = TRUE
%% Cell type:code id:62fe69ce tags:
``` prob
:check invariant
```
%%%% Output: execute_result
|Predicate|Value|
|---|---|
|a∈0‥x|TRUE|
|b∈1‥y|TRUE|
a:0..x = TRUE
b:1..y = TRUE
%% Cell type:code id:d2054303 tags:
``` prob
:check assertions
```
%%%% Output: execute_result
|Predicate|Value|
|---|---|
|a≤x|TRUE|
|b≤y|TRUE|
a<=x = TRUE
b<=y = TRUE
%% Cell type:markdown id:72e11ab6 tags:
TODO: Test for Event-B
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());
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment