make ExplicitChecks LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/Other
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/ExplicitChecks.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar ExplicitChecks.java
java -cp .:btypes.jar ExplicitChecks mixed 1 false
INVARIANT VIOLATED
COUNTER EXAMPLE TRACE:

_get_x: 0
Number of States: 2
Number of Transitions: 2

It should be possible to apply model checking, deactivating checking invariants or deadlocks

It should be possible to apply model checking, searching for a goal

I get this message when using a model with <->:

Exception in thread "main" java.lang.RuntimeException: Given operator is not implemented: SET_RELATION
at de.hhu.stups.codegenerator.generators.ExpressionGenerator.generateExpression(ExpressionGenerator.java:349)
at de.hhu.stups.codegenerator.generators.ExpressionGenerator.visitExprOperatorNode(ExpressionGenerator.java:239)

java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/tictac.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar tictac.java
tictac.java:127: error: incompatible types: no instance(s) of type variable(s) S,T exist so that BRelation<S,T> conforms to BSet<BTuple<BInteger,BInteger>>
return square.checkDomain(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3)))).and(square.checkRange(BSet.interval(new BInteger(0), new BInteger(1)))).and(square.isFunction()).and(square.isPartial(BRelation.cartesianProduct(BSet.interval(new BInteger(1), new BInteger(3)), BSet.interval(new BInteger(1), new BInteger(3))))).booleanValue();
...

$ time make SetLaws LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/Other
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/SetLaws.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar SetLaws.java
SetLaws.java:560: error: incompatible types: BSet cannot be converted to BSet<BSet>
for(BSet _ic_ss_1 : SS.pow().difference(SS)) {
^
Note: Some messages have been simplified; recompile with -Xdiags:verbose to get full output
1 error
make: *** [SetLaws] Error 1

make LargeFunction LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/micro
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/micro/LargeFunction.mch
cp benchmarks/model_checking/ProB/micro/*.java .
javac -cp .:btypes.jar LargeFunction.java
LargeFunction.java:66: error: incompatible types: BRelation<BInteger,BInteger> cannot be converted to BRelation<BTuple<BInteger,BInteger>,BInteger>
BRelation<BTuple<BInteger, BInteger>, BInteger> _ic_set_0 = new BRelation<BInteger, BInteger>();
^
LargeFunction.java:69: error: no suitable constructor found for BRelation(BTuple<BInteger,BInteger>)
_ic_set_0 = _ic_set_0.union(new BRelation<BTuple<BInteger, BInteger>, BInteger>(new BTuple<>(_ic_y_1, _ic_x_1.plus(_ic_y_1).modulo(n))));
^
constructor BRelation.BRelation(PersistentHashMap) is not applicable
(argument mismatch; cannot infer type arguments for BTuple<>
reason: no instance(s) of type variable(s) S,T exist so that BTuple<S,T> conforms to PersistentHashMap)
constructor BRelation.BRelation(BTuple<BTuple<BInteger,BInteger>,BInteger>...) is not applicable
(varargs mismatch; cannot infer type arguments for BTuple<>
reason: inference variable S has incompatible bounds
equality constraints: BTuple<BInteger,BInteger>
lower bounds: BInteger)
where S,T are type-variables:
S extends Object declared in class BTuple
T extends Object declared in class BTuple
2 errors
make: *** [LargeFunction] Error 1

Java

./gradlew run -Planguage="java" -Pbig_integer="true/false" [-Pminint="minint" -Pmaxint="maxint"] -Pdeferred_set_size="size" -Pfile="<path_relative_to_project_directory>"

--Build is sucessful but getting wrong no of arguments. Can you pls update on this?

This could be treated similar to constructs like x : NATURAL (which does not generate the infinite set NATURAL, but checks whether x >= 0 instead).

One of such operator is interval. E.g. x : 0..5 should not generate the set with all elements in 0..5, but rather checks whether x >= 0 & x <= 5

Other operators could be improved as well (see kernel_mappings.pl in ProB Prolog: binary_in_boolean_type/2, binary_not_in_boolean_type/2, unary_in_boolean_type/2, unary_not_in_boolean_type/2)

Currently, EXTENDS is treated similar to INCLUDES and is thus too strict. When extending another machine, it should be possible to access its INITIALISATION and OPERATIONS. It also seems that INITIALISATION is not optional in the ANTLR B parser. This should be fixed as well

For the model below I get this exception:

java -jar b2program/build/libs/B2Program-all-0.1.0-SNAPSHOT.jar java false -2147483648 2147483647 10 true true QueensWithEvents.mch

Exception in thread "main" java.lang.IndexOutOfBoundsException: Index 1 out of bounds for length 1
at java.base/jdk.internal.util.Preconditions.outOfBounds(Preconditions.java:64)
at java.base/jdk.internal.util.Preconditions.outOfBoundsCheckIndex(Preconditions.java:70)
at java.base/jdk.internal.util.Preconditions.checkIndex(Preconditions.java:248)
at java.base/java.util.Objects.checkIndex(Objects.java:359)
at java.base/java.util.ArrayList.get(ArrayList.java:427)
at de.hhu.stups.codegenerator.generators.PredicateGenerator.transformPowNodeToRelationNode(PredicateGenerator.java:123)
at de.hhu.stups.codegenerator.generators.PredicateGenerator.generateRelationOnRhs(PredicateGenerator.java:110)
at de.hhu.stups.codegenerator.generators.PredicateGenerator.visitPredicateOperatorWithExprArgs(PredicateGenerator.java:96)
at de.hhu.stups.codegenerator.generators.MachineGenerator.visitPredicateOperatorWithExprArgs(MachineGenerator.java:437)
at de.hhu.stups.codegenerator.generators.MachineGenerator.visitPredicateOperatorWithExprArgs(MachineGenerator.java:75)
at de.prob.parser.ast.visitors.generic.ParametrisedPredicateVisitor.visitPredicateNode(ParametrisedPredicateVisitor.java:17)
at de.hhu.stups.codegenerator.generators.PredicateGenerator.lambda$visitPredicateOperatorNode$0(PredicateGenerator.java:82)

This should be support when there is a singleton set on the right-hand side which stores a constant value

when commenting in

( #(f,y).((f = %x.(x : 0..100|x + y) & y=1000 & f(5) = 1005)) )

we get this error

make ExplicitChecks LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/Other
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/ExplicitChecks.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar ExplicitChecks.java
ExplicitChecks.java:156: error: cannot find symbol
_ic_set_7 = _ic_set_7.union(new BRelation<BInteger, BInteger>(new BTuple<>(_ic_x_1, _ic_x_1.plus(y))));
^
symbol: variable y
location: class ExplicitChecks
1 error

This feature is already implemented for JavaScript. It should also be implemented for Java and C++ for validation purposes.

java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/StringLaws.mch
cp benchmarks/model_checking/ProB/Other/*.java .
javac -cp .:btypes.jar StringLaws.java
StringLaws.java:147: error: cannot find symbol
return new BBoolean((!s1.equal(s2).booleanValue() || s2.equal(s1).booleanValue()) && (!s2.equal(s1).booleanValue() || s1.equal(s2).booleanValue())).booleanValue();
^
symbol: method equal(BString)
location: variable s1 of type BString
StringLaws.java:147: error: cannot find symbol
return new BBoolean((!s1.equal(s2).booleanValue() || s2.equal(s1).booleanValue()) && (!s2.equal(s1).booleanValue() || s1.equal(s2).booleanValue())).booleanValue();

import de.prob.parser.ast.nodes.DeclarationNode;
import de.prob.parser.ast.nodes.expression.ExprNode;
import de.prob.parser.ast.nodes.expression.ExpressionOperatorNode;
import de.prob.parser.ast.nodes.expression.IdentifierExprNode;
import de.prob.parser.ast.nodes.expression.NumberNode;
import de.prob.parser.ast.nodes.predicate.PredicateNode;
import de.prob.parser.ast.nodes.predicate.PredicateOperatorNode;
import de.prob.parser.ast.nodes.predicate.PredicateOperatorWithExprArgsNode;
etc are missing. The external jar files are not available online either.
Any leads on this will be highly appreciated.

When an invariant violation is detected, the feedback should be improved by showing the violated conjunct

Currently, it is not possible to write pruning predicates. For n bounded variables, the first n predicates/conjuncts must always constraint the quantified variables in the order they are defined. Pruning predicates should be allowed in the future.

Furthermore, it is not possible to use multiple bounded variables in the first predicates even though they are enumerated in the order they are defined. For example, one must always write a : dom(X) & b : ran(X) & a |-> b : X instead of a |-> b : X directly. This should also be improved in the future.
First, think about iterating over X directly. If this would not really improve the performance, we could treat this as syntactical sugar which is then rewritten to automatically

Currently, we only have tests for simulation. We should also implement some integration tests for model checking

• VisB Events should execute events with parameters from visualization instead of Operations View
• Implement SimB

For nested quantified constructs, there are possible name collisions leading to a parse error:

operation(frnt,nxt) =
    SELECT frnt : ... & nxt : ran(next) & !nxt(...)