ProB Logic Calculator

2017-10-06T07:53:15Z

Jens Bendisposto:

Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial|small tutorial]] at the bottom of the page.

[[Image:EvalB.png|600px |link=http://wyvern.cs.uni-duesseldorf.de:8443/index.html]]



[http://wyvern.cs.uni-duesseldorf.de:8443/index.html Start ProB Logic Calculator].

The above calculator has a time-out of 3 seconds, and <tt>MAXINT</tt> is set to 127 and <tt>MININT</tt> to -128.

You can also [[Download|download ProB]] for execution on your computer, along with support for [http://en.wikipedia.org/wiki/B B], [http://www.event-b.org/ Event-B], [http://en.wikipedia.org/wiki/Communicating_sequential_processes CSP-M],
[http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+], and [http://en.wikipedia.org/wiki/Z_notation Z].

Short syntax guide for some of B's constructs:
* comments <tt>/* ... */</tt>
* conjunction <tt>P & Q</tt>, disjunction <tt>P or Q</tt>, implication <tt>P => Q</tt>, equivalence <tt>P <=> Q</tt>, negation <tt>not(P)</tt>, existential quantification <tt>#x.(P)</tt>, universal quantification <tt>!x.(P=>Q)</tt>
* equality <tt>x=y</tt>, disequality <tt>x/=y</tt>
* boolean values <tt>TRUE</tt>, <tt>FALSE</tt>, converting predicate to value <tt>bool(P)</tt>; Warning: <tt>TRUE</tt> and <tt>FALSE</tt> are values and <em>not</em> predicates in B and cannot be combined using logical connectives.
* strings <tt>"..."</tt>, set of all strings <tt>STRING</tt>
* arithmetic comparisons <tt>x < y</tt>, <tt>x > y</tt>, <tt>x <= y</tt>, <tt>x >= y</tt>
* membership <tt>x:S</tt>, not membership, <tt>x/:S</tt>, subset <tt>S<:R</tt>, strict subset <tt>S <<: R</tt>
* arithmetic operators <tt>x+y</tt>, <tt>x-y</tt>, <tt>x*y</tt>, <tt>x/y</tt>, <tt>x mod y</tt>, <tt>x**y</tt> , <tt>succ(x)</tt>, <tt>pred(x)</tt>
* mathematical integers <tt>INTEGER</tt>, mathematical natural numbers <tt>NATURAL</tt>, implementable integers <tt>INT</tt>, implementable naturals <tt>NAT</tt>, maximum implementable integer <tt>MAXINT</tt>, minimum implementable integer <tt>MININT</tt>
* empty set <tt>{}</tt>, set enumeration <tt>{x,y,...}</tt>, comprehension set defined by predicate <tt>{x|P}</tt>, lambda abstraction <tt>%x.(P|E)</tt>, interval <tt>m..n</tt>
* set union <tt>S \/ T</tt>, set intersection <tt>S /\ T</tt>, set difference <tt>S - T</tt>, power set <tt>POW(S)</tt>, Cartesian product <tt>S*T</tt>, cardinality of set <tt>card(S)</tt>
* set of relations between two sets <tt>S <-> T</tt>, set of partial functions <tt>S +-> T</tt>, set of total functions <tt>S --> T</tt>
* relational image <tt>r[S]</tt>, relational composition <tt>(r1 ; r2)</tt>, transitive closure <tt>closure1(r)</tt>, identity relation over a set <tt>id(S)</tt>, domain of a relation <tt>dom(r)</tt>, its range <tt>ran(r)</tt>, its inverse <tt>r~</tt>, relational overriding <tt>r1 <+ r2</tt>
* empty sequence <tt>[]</tt>, explicit sequence <tt>[x,y,...]</tt>, concatenation <tt>s1^s2</tt>, first element <tt>first(s)</tt>, tail <tt>tail(s)</tt>, prepend an element <tt>E->s</tt>, size of a sequence <tt>size(s)</tt>
* sets of sequences over a set <tt>seq(S)</tt>, set of injective sequences <tt>iseq(S)</tt>, set of permutations <tt>perm(S)</tt>
More details can be found on our [[Summary_of_B_Syntax|page on the B syntax]]. Note: statements (aka substitutions) and B machine construction elements cannot be used above; you must enter either a predicate or an expression.

The term <em>logic calculator</em> is taken over from [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html Leslie Lamport].
An early implementation of a logic calculator is the [http://en.wikipedia.org/wiki/William_Stanley_Jevons#Logic Logic Piano].

We are grateful for feedback about our logic calculator (send an email to [http://www.stups.uni-duesseldorf.de/~leuschel Michael Leuschel]).
You can also switch the calculator into [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] mode.
In future we plan to provide additional features:
* getting an unsat core for unsatisfiable formulas
* better feedback for syntax and type errors
* graphical visualization of formulas and models
* support for further alternative input syntax, such as [http://en.wikipedia.org/wiki/Z_notation Z]
* ability to change the parameters, e.g., use the [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 ProB-Kodkod backend] instead of the default constraint-logic programming kernel.

== Small Tutorial ==

Here is a small tutorial to get you started.
B distinguishes <em>expressions</em>, which have a value, and <em>predicates</em> which can be either true or false.
First, let us type an expression:
1+1
The calculator returns the value <tt>2</tt>.
A more complicated expression is:
{1,2,3} \/ {1+2+3}
which has the value <tt>{1,2,3,6}</tt>.
Now, let us type a simple predicate:
1>2
The calculator tells us that this predicate is false.
We can combine predicates using the logical connectives.
For example, the following predicate is true:
1>2 or 2>1
We can also use existential quantification to produce a predicate:
#(x).(x+10=30)
which is true and ProB will give you a solution <tt>x=20</tt>.
In the calculator, any variable that is not explicitly introduced is considered existentially quantified. Thus, you get the same effect by simply typing:
x+10=30
If you want to get all solutions for the equation x+10=30, you can make use of a set comprehension:
{x|x+10=30}
Here the calculator will compute the value of the expression to be <tt>{20}</tt>, i.e., we know that 20 is the only solution for <tt>x</tt>.
Note that the B language has Boolean values <tt>TRUE</tt> and <tt>FALSE</tt>, but these are <em>not</em> considered predicates in B.
Thus if we type:
TRUE
this is considered an expression and not a predicate.
This also means that <tt>TRUE or FALSE</tt> is not considered a legal predicate in pure B.
However, for convenience, the logic calculator accepts this and as such you can type:
TRUE or FALSE
which is determined to be true.
In pure B, you would have to write something like:
1=1 or 1=2
Finally, in pure B, variables can only range over values in B, not over predicates. Thus <tt>P or Q</tt> is not allowed in pure B, but our logic calculator does accept it.
As such you can type
P or Q
which is equivalent to typing
P=TRUE or Q=TRUE
If you want to find all models of the formula, you can use a set comprehension:
{P,Q | P or Q}
Also, if you want to check whether your formula is a tautology you can select the "Universal (Checking)" entry in the Quantification Mode menu. In this case (for <tt>P or Q</tt>) a counter example is produced by the tool.
More generally, you can check proof rules using the "Tautology Check" button.
E.g., our tool will confirm that the following is a tautology:
(A => B) & not(B) => not(A)
Note, however, that our tool is <em>not</em> a prover in general: you can use it to find solutions and counter-examples, but in general it cannot be used to prove formulas using variables with infinite type.
In those cases, you may see enumeration warnings in the output, which means that ProB was only able to check a finite number of values from an infinite set. This could mean that the result displayed is not correct (even though in general solutions and counter-examples tend to be correct; in future we will refine ProB's output to also indicate when the solution/counter-example is still guaranteed to be correct)!

== Executing the Calculator locally ==
You can evaluate formulas on your machine in the same way as the calculator above, by [[Download|downloading ProB]] (ideally a nightly build) and then executing one of the following commands:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE
The above command requires you to put the formula into a file <tt>MYFILE</tt>.
The command below allows you to put the formula directly into the command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval "MYFORMULA"
If you want to perform the tautology check you have to do the following using the -eval_rule_file command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE
You can also start your own REPL using the -repl command (you may wish to use the rlwrap tool):
./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128
You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...) according to your needs; the [[Using_the_Command-Line_Version_of_ProB|user manual]] provides more details.
You may wish to use the rlwrap tool:
rlwrap ./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128

Probably, you may want to generate full-fledged B machines as input to <tt>probcli</tt>.
This allows you to introduce enumerated and deferred sets; compared to using sets of strings, this has benefits in terms of more stringent typechecking and more efficient constraint solving.

An alternate front-end to the calculator is [http://wyvern.cs.uni-duesseldorf.de:8443/ available here].
Its code is available at <tt>https://github.com/bendisposto/evalB</tt>.

ProB Logic Calculator

2017-10-04T15:22:10Z

Jens Bendisposto:

Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial|small tutorial]] at the bottom of the page.

<html>
<iframe src="http://wyvern.cs.uni-duesseldorf.de:8443/embedded.html" width="780" height="450" border="0" frameborder="0" scrolling="no">
<p>Your Browser does not suport IFrames.</p>
</iframe>
</html>

The above calculator has a time-out of 3 seconds, and <tt>MAXINT</tt> is set to 127 and <tt>MININT</tt> to -128.
A front-end with larger text areas is [http://wyvern.cs.uni-duesseldorf.de:8080/evalB/index.html available here].
An alternative, older version of the calculator is available at the [http://www.formalmind.com/en/blog/prob-logic-calculator Formal Mind website].
You can also [[Download|download ProB]] for execution on your computer, along with support for [http://en.wikipedia.org/wiki/B B], [http://www.event-b.org/ Event-B], [http://en.wikipedia.org/wiki/Communicating_sequential_processes CSP-M],
[http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+], and [http://en.wikipedia.org/wiki/Z_notation Z]. There are also 64-bit versions available for Linux and Mac (the above calculator only uses the 32-bit version).

Short syntax guide for some of B's constructs:
* comments <tt>/* ... */</tt>
* conjunction <tt>P & Q</tt>, disjunction <tt>P or Q</tt>, implication <tt>P => Q</tt>, equivalence <tt>P <=> Q</tt>, negation <tt>not(P)</tt>, existential quantification <tt>#x.(P)</tt>, universal quantification <tt>!x.(P=>Q)</tt>
* equality <tt>x=y</tt>, disequality <tt>x/=y</tt>
* boolean values <tt>TRUE</tt>, <tt>FALSE</tt>, converting predicate to value <tt>bool(P)</tt>; Warning: <tt>TRUE</tt> and <tt>FALSE</tt> are values and <em>not</em> predicates in B and cannot be combined using logical connectives.
* strings <tt>"..."</tt>, set of all strings <tt>STRING</tt>
* arithmetic comparisons <tt>x < y</tt>, <tt>x > y</tt>, <tt>x <= y</tt>, <tt>x >= y</tt>
* membership <tt>x:S</tt>, not membership, <tt>x/:S</tt>, subset <tt>S<:R</tt>, strict subset <tt>S <<: R</tt>
* arithmetic operators <tt>x+y</tt>, <tt>x-y</tt>, <tt>x*y</tt>, <tt>x/y</tt>, <tt>x mod y</tt>, <tt>x**y</tt> , <tt>succ(x)</tt>, <tt>pred(x)</tt>
* mathematical integers <tt>INTEGER</tt>, mathematical natural numbers <tt>NATURAL</tt>, implementable integers <tt>INT</tt>, implementable naturals <tt>NAT</tt>, maximum implementable integer <tt>MAXINT</tt>, minimum implementable integer <tt>MININT</tt>
* empty set <tt>{}</tt>, set enumeration <tt>{x,y,...}</tt>, comprehension set defined by predicate <tt>{x|P}</tt>, lambda abstraction <tt>%x.(P|E)</tt>, interval <tt>m..n</tt>
* set union <tt>S \/ T</tt>, set intersection <tt>S /\ T</tt>, set difference <tt>S - T</tt>, power set <tt>POW(S)</tt>, Cartesian product <tt>S*T</tt>, cardinality of set <tt>card(S)</tt>
* set of relations between two sets <tt>S <-> T</tt>, set of partial functions <tt>S +-> T</tt>, set of total functions <tt>S --> T</tt>
* relational image <tt>r[S]</tt>, relational composition <tt>(r1 ; r2)</tt>, transitive closure <tt>closure1(r)</tt>, identity relation over a set <tt>id(S)</tt>, domain of a relation <tt>dom(r)</tt>, its range <tt>ran(r)</tt>, its inverse <tt>r~</tt>, relational overriding <tt>r1 <+ r2</tt>
* empty sequence <tt>[]</tt>, explicit sequence <tt>[x,y,...]</tt>, concatenation <tt>s1^s2</tt>, first element <tt>first(s)</tt>, tail <tt>tail(s)</tt>, prepend an element <tt>E->s</tt>, size of a sequence <tt>size(s)</tt>
* sets of sequences over a set <tt>seq(S)</tt>, set of injective sequences <tt>iseq(S)</tt>, set of permutations <tt>perm(S)</tt>
More details can be found on our [[Summary_of_B_Syntax|page on the B syntax]]. Note: statements (aka substitutions) and B machine construction elements cannot be used above; you must enter either a predicate or an expression.

The term <em>logic calculator</em> is taken over from [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html Leslie Lamport].
An early implementation of a logic calculator is the [http://en.wikipedia.org/wiki/William_Stanley_Jevons#Logic Logic Piano].

We are grateful for feedback about our logic calculator (send an email to [http://www.stups.uni-duesseldorf.de/~leuschel Michael Leuschel]).
You can also switch the calculator into [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] mode.
In future we plan to provide additional features:
* getting an unsat core for unsatisfiable formulas
* better feedback for syntax and type errors
* graphical visualization of formulas and models
* support for further alternative input syntax, such as [http://en.wikipedia.org/wiki/Z_notation Z]
* ability to change the parameters, e.g., use the [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 ProB-Kodkod backend] instead of the default constraint-logic programming kernel.

== Small Tutorial ==

Here is a small tutorial to get you started.
B distinguishes <em>expressions</em>, which have a value, and <em>predicates</em> which can be either true or false.
First, let us type an expression:
1+1
The calculator returns the value <tt>2</tt>.
A more complicated expression is:
{1,2,3} \/ {1+2+3}
which has the value <tt>{1,2,3,6}</tt>.
Now, let us type a simple predicate:
1>2
The calculator tells us that this predicate is false.
We can combine predicates using the logical connectives.
For example, the following predicate is true:
1>2 or 2>1
We can also use existential quantification to produce a predicate:
#(x).(x+10=30)
which is true and ProB will give you a solution <tt>x=20</tt>.
In the calculator, any variable that is not explicitly introduced is considered existentially quantified. Thus, you get the same effect by simply typing:
x+10=30
If you want to get all solutions for the equation x+10=30, you can make use of a set comprehension:
{x|x+10=30}
Here the calculator will compute the value of the expression to be <tt>{20}</tt>, i.e., we know that 20 is the only solution for <tt>x</tt>.
Note that the B language has Boolean values <tt>TRUE</tt> and <tt>FALSE</tt>, but these are <em>not</em> considered predicates in B.
Thus if we type:
TRUE
this is considered an expression and not a predicate.
This also means that <tt>TRUE or FALSE</tt> is not considered a legal predicate in pure B.
However, for convenience, the logic calculator accepts this and as such you can type:
TRUE or FALSE
which is determined to be true.
In pure B, you would have to write something like:
1=1 or 1=2
Finally, in pure B, variables can only range over values in B, not over predicates. Thus <tt>P or Q</tt> is not allowed in pure B, but our logic calculator does accept it.
As such you can type
P or Q
which is equivalent to typing
P=TRUE or Q=TRUE
If you want to find all models of the formula, you can use a set comprehension:
{P,Q | P or Q}
Also, if you want to check whether your formula is a tautology you can select the "Universal (Checking)" entry in the Quantification Mode menu. In this case (for <tt>P or Q</tt>) a counter example is produced by the tool.
More generally, you can check proof rules using the "Tautology Check" button.
E.g., our tool will confirm that the following is a tautology:
(A => B) & not(B) => not(A)
Note, however, that our tool is <em>not</em> a prover in general: you can use it to find solutions and counter-examples, but in general it cannot be used to prove formulas using variables with infinite type.
In those cases, you may see enumeration warnings in the output, which means that ProB was only able to check a finite number of values from an infinite set. This could mean that the result displayed is not correct (even though in general solutions and counter-examples tend to be correct; in future we will refine ProB's output to also indicate when the solution/counter-example is still guaranteed to be correct)!

== Executing the Calculator locally ==
You can evaluate formulas on your machine in the same way as the calculator above, by [[Download|downloading ProB]] (ideally a nightly build) and then executing one of the following commands:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE
The above command requires you to put the formula into a file <tt>MYFILE</tt>.
The command below allows you to put the formula directly into the command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval "MYFORMULA"
If you want to perform the tautology check you have to do the following using the -eval_rule_file command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE
You can also start your own REPL using the -repl command (you may wish to use the rlwrap tool):
./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128
You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...) according to your needs; the [[Using_the_Command-Line_Version_of_ProB|user manual]] provides more details.
You may wish to use the rlwrap tool:
rlwrap ./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128

Probably, you may want to generate full-fledged B machines as input to <tt>probcli</tt>.
This allows you to introduce enumerated and deferred sets; compared to using sets of strings, this has benefits in terms of more stringent typechecking and more efficient constraint solving.

An alternate front-end to the calculator is [http://wyvern.cs.uni-duesseldorf.de:8443/ available here].
Its code is available at <tt>https://github.com/bendisposto/evalB</tt>.

ProB Logic Calculator

2017-10-04T15:21:31Z

Jens Bendisposto:

Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial|small tutorial]] at the bottom of the page.

<html>
<iframe src="https://wyvern.cs.uni-duesseldorf.de:8443/embedded.html" width="780" height="450" border="0" frameborder="0" scrolling="no">
<p>Your Browser does not suport IFrames.</p>
</iframe>
</html>

The above calculator has a time-out of 3 seconds, and <tt>MAXINT</tt> is set to 127 and <tt>MININT</tt> to -128.
A front-end with larger text areas is [http://wyvern.cs.uni-duesseldorf.de:8080/evalB/index.html available here].
An alternative, older version of the calculator is available at the [http://www.formalmind.com/en/blog/prob-logic-calculator Formal Mind website].
You can also [[Download|download ProB]] for execution on your computer, along with support for [http://en.wikipedia.org/wiki/B B], [http://www.event-b.org/ Event-B], [http://en.wikipedia.org/wiki/Communicating_sequential_processes CSP-M],
[http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+], and [http://en.wikipedia.org/wiki/Z_notation Z]. There are also 64-bit versions available for Linux and Mac (the above calculator only uses the 32-bit version).

Short syntax guide for some of B's constructs:
* comments <tt>/* ... */</tt>
* conjunction <tt>P & Q</tt>, disjunction <tt>P or Q</tt>, implication <tt>P => Q</tt>, equivalence <tt>P <=> Q</tt>, negation <tt>not(P)</tt>, existential quantification <tt>#x.(P)</tt>, universal quantification <tt>!x.(P=>Q)</tt>
* equality <tt>x=y</tt>, disequality <tt>x/=y</tt>
* boolean values <tt>TRUE</tt>, <tt>FALSE</tt>, converting predicate to value <tt>bool(P)</tt>; Warning: <tt>TRUE</tt> and <tt>FALSE</tt> are values and <em>not</em> predicates in B and cannot be combined using logical connectives.
* strings <tt>"..."</tt>, set of all strings <tt>STRING</tt>
* arithmetic comparisons <tt>x < y</tt>, <tt>x > y</tt>, <tt>x <= y</tt>, <tt>x >= y</tt>
* membership <tt>x:S</tt>, not membership, <tt>x/:S</tt>, subset <tt>S<:R</tt>, strict subset <tt>S <<: R</tt>
* arithmetic operators <tt>x+y</tt>, <tt>x-y</tt>, <tt>x*y</tt>, <tt>x/y</tt>, <tt>x mod y</tt>, <tt>x**y</tt> , <tt>succ(x)</tt>, <tt>pred(x)</tt>
* mathematical integers <tt>INTEGER</tt>, mathematical natural numbers <tt>NATURAL</tt>, implementable integers <tt>INT</tt>, implementable naturals <tt>NAT</tt>, maximum implementable integer <tt>MAXINT</tt>, minimum implementable integer <tt>MININT</tt>
* empty set <tt>{}</tt>, set enumeration <tt>{x,y,...}</tt>, comprehension set defined by predicate <tt>{x|P}</tt>, lambda abstraction <tt>%x.(P|E)</tt>, interval <tt>m..n</tt>
* set union <tt>S \/ T</tt>, set intersection <tt>S /\ T</tt>, set difference <tt>S - T</tt>, power set <tt>POW(S)</tt>, Cartesian product <tt>S*T</tt>, cardinality of set <tt>card(S)</tt>
* set of relations between two sets <tt>S <-> T</tt>, set of partial functions <tt>S +-> T</tt>, set of total functions <tt>S --> T</tt>
* relational image <tt>r[S]</tt>, relational composition <tt>(r1 ; r2)</tt>, transitive closure <tt>closure1(r)</tt>, identity relation over a set <tt>id(S)</tt>, domain of a relation <tt>dom(r)</tt>, its range <tt>ran(r)</tt>, its inverse <tt>r~</tt>, relational overriding <tt>r1 <+ r2</tt>
* empty sequence <tt>[]</tt>, explicit sequence <tt>[x,y,...]</tt>, concatenation <tt>s1^s2</tt>, first element <tt>first(s)</tt>, tail <tt>tail(s)</tt>, prepend an element <tt>E->s</tt>, size of a sequence <tt>size(s)</tt>
* sets of sequences over a set <tt>seq(S)</tt>, set of injective sequences <tt>iseq(S)</tt>, set of permutations <tt>perm(S)</tt>
More details can be found on our [[Summary_of_B_Syntax|page on the B syntax]]. Note: statements (aka substitutions) and B machine construction elements cannot be used above; you must enter either a predicate or an expression.

The term <em>logic calculator</em> is taken over from [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html Leslie Lamport].
An early implementation of a logic calculator is the [http://en.wikipedia.org/wiki/William_Stanley_Jevons#Logic Logic Piano].

We are grateful for feedback about our logic calculator (send an email to [http://www.stups.uni-duesseldorf.de/~leuschel Michael Leuschel]).
You can also switch the calculator into [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] mode.
In future we plan to provide additional features:
* getting an unsat core for unsatisfiable formulas
* better feedback for syntax and type errors
* graphical visualization of formulas and models
* support for further alternative input syntax, such as [http://en.wikipedia.org/wiki/Z_notation Z]
* ability to change the parameters, e.g., use the [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 ProB-Kodkod backend] instead of the default constraint-logic programming kernel.

== Small Tutorial ==

Here is a small tutorial to get you started.
B distinguishes <em>expressions</em>, which have a value, and <em>predicates</em> which can be either true or false.
First, let us type an expression:
1+1
The calculator returns the value <tt>2</tt>.
A more complicated expression is:
{1,2,3} \/ {1+2+3}
which has the value <tt>{1,2,3,6}</tt>.
Now, let us type a simple predicate:
1>2
The calculator tells us that this predicate is false.
We can combine predicates using the logical connectives.
For example, the following predicate is true:
1>2 or 2>1
We can also use existential quantification to produce a predicate:
#(x).(x+10=30)
which is true and ProB will give you a solution <tt>x=20</tt>.
In the calculator, any variable that is not explicitly introduced is considered existentially quantified. Thus, you get the same effect by simply typing:
x+10=30
If you want to get all solutions for the equation x+10=30, you can make use of a set comprehension:
{x|x+10=30}
Here the calculator will compute the value of the expression to be <tt>{20}</tt>, i.e., we know that 20 is the only solution for <tt>x</tt>.
Note that the B language has Boolean values <tt>TRUE</tt> and <tt>FALSE</tt>, but these are <em>not</em> considered predicates in B.
Thus if we type:
TRUE
this is considered an expression and not a predicate.
This also means that <tt>TRUE or FALSE</tt> is not considered a legal predicate in pure B.
However, for convenience, the logic calculator accepts this and as such you can type:
TRUE or FALSE
which is determined to be true.
In pure B, you would have to write something like:
1=1 or 1=2
Finally, in pure B, variables can only range over values in B, not over predicates. Thus <tt>P or Q</tt> is not allowed in pure B, but our logic calculator does accept it.
As such you can type
P or Q
which is equivalent to typing
P=TRUE or Q=TRUE
If you want to find all models of the formula, you can use a set comprehension:
{P,Q | P or Q}
Also, if you want to check whether your formula is a tautology you can select the "Universal (Checking)" entry in the Quantification Mode menu. In this case (for <tt>P or Q</tt>) a counter example is produced by the tool.
More generally, you can check proof rules using the "Tautology Check" button.
E.g., our tool will confirm that the following is a tautology:
(A => B) & not(B) => not(A)
Note, however, that our tool is <em>not</em> a prover in general: you can use it to find solutions and counter-examples, but in general it cannot be used to prove formulas using variables with infinite type.
In those cases, you may see enumeration warnings in the output, which means that ProB was only able to check a finite number of values from an infinite set. This could mean that the result displayed is not correct (even though in general solutions and counter-examples tend to be correct; in future we will refine ProB's output to also indicate when the solution/counter-example is still guaranteed to be correct)!

== Executing the Calculator locally ==
You can evaluate formulas on your machine in the same way as the calculator above, by [[Download|downloading ProB]] (ideally a nightly build) and then executing one of the following commands:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE
The above command requires you to put the formula into a file <tt>MYFILE</tt>.
The command below allows you to put the formula directly into the command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval "MYFORMULA"
If you want to perform the tautology check you have to do the following using the -eval_rule_file command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE
You can also start your own REPL using the -repl command (you may wish to use the rlwrap tool):
./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128
You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...) according to your needs; the [[Using_the_Command-Line_Version_of_ProB|user manual]] provides more details.
You may wish to use the rlwrap tool:
rlwrap ./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128

Probably, you may want to generate full-fledged B machines as input to <tt>probcli</tt>.
This allows you to introduce enumerated and deferred sets; compared to using sets of strings, this has benefits in terms of more stringent typechecking and more efficient constraint solving.

An alternate front-end to the calculator is [http://wyvern.cs.uni-duesseldorf.de:8443/ available here].
Its code is available at <tt>https://github.com/bendisposto/evalB</tt>.

ProB Java API

2016-09-30T08:09:16Z

Jens Bendisposto: /* Additional Material */

[[Category:Components]]
[[Category:ProB Java API]]

== Documentation ==
<p class="btn btn-lg btn-outline">
<i class="fa fa-road"></i> [[ProB Java API Tutorial | Tutorial]]
</p>
<p class="btn btn-lg btn-outline">
<i class="fa fa-cog"></i> [http://nightly.cobra.cs.uni-duesseldorf.de/prob2/prob2-handbook/nightly/devel/html Developer Manual]
</p>

== Additional Material ==
*[[ProB 2.0 Development]]
*[[Programmatic_Abstractions_in_the_ProB_2.0_API]]
*[https://docs.google.com/document/pub?id=109z3qG6_KBUqm0NC9FaEF1C6_NYCJl453wcXzbovj2Q ProB 2.0 Requirements Document] <br/>(if you want to comment on the Document, please use goo.gl/KS2bh)

*[[Media:Extending prob.pdf|Rodin User and Developer Workshop 2012 - Tutorial Presentation]]

*[[Tutorial13|Rodin User and Developer Workshop 2013 - Tutorial]]

*[[ProB 2.0 within Rodin and a HTML Visualization Example]]

== Download ==

Nightly builds of ProB 2 for Rodin 3 can be obtained from within Rodin using the update site [http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/nightly/ http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/nightly/].

Bugs

2016-07-29T12:46:42Z

Jens Bendisposto:

The ProB Animator and Model Checker

2015-10-15T11:17:14Z

Jens Bendisposto: /* Implementation */

{| cellpadding="5"
|-valign="top"
|width="60%" style="padding-right:20px;" |ProB is an animator, constraint solver and model checker for the [http://en.wikipedia.org/wiki/B-Method B-Method] (see the [http://www.clearsy.com/en/our-specific-know-how/b-method/?lang=en B-Method site of Clearsy]). It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation.

In addition to the B language, ProB also supports [http://www.event-b.org/ Event-B], [http://en.wikipedia.org/wiki/Communicating_sequential_processes CSP-M],
[http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+], and [http://en.wikipedia.org/wiki/Z_notation Z]. ProB can be installed within [http://sourceforge.net/projects/rodin-b-sharp/ Rodin], where it comes with [http://www.stups.uni-duesseldorf.de/BMotionStudio/ BMotionStudio] to easily generate domain specific graphical visualizations.

ProB is being used within Siemens, Alstom, and several other companies for [http://www.data-validation.fr data validation] of complicated properties for safety critical systems. Commercial support is provided by the spin-off company [http://www.formalmind.com Formal Mind].

Part of the research and development was conducted within various research projects, such as the [http://www.epsrc.ac.uk/default.htm EPSRC] funded projects [http://users.ecs.soton.ac.uk/phh/abcd/ ABCD] and [http://users.ecs.soton.ac.uk/mal/ISM.html iMoc], the EU funded projects [http://rodin.cs.ncl.ac.uk/ Rodin], [http://www.deploy-project.eu/ Deploy] and [http://www.advance-ict.eu/ Advance] as well as the [http://www.dfg.de/ DFG] project [http://www.gepavas.de/ Gepavas].

Automatically generated test [http://nightly.cobra.cs.uni-duesseldorf.de/coverage/html/ coverage reports are available].

|width="40%" style="background:#EDF2F2;padding:15px;" | '''News'''
'''19/2/2015'''
[[Download|ProB 1.5.0]] is available. Highlights: improved random enumeration, MACE/SEM style static symmetry reduction for deferred set elements, MC/DC coverage analysis for guards and invariants, improved TLC interface, bug fixes and improvements including but not limited to the constraint solver.

'''3/6/2014'''
ProB supports [[Event-B Theories]].

'''30/03/2012'''
A first version of the online [[ProB_Logic_Calculator|ProB Logic Calculator]] is available.

''' '''
[[Download#Short Release History|More in Release History]]
|}

== Implementation ==
The core of ProB is implemented in [http://www.sics.se/isl/sicstuswww/site/index.html SICStus Prolog] (but can be run without a SICStus Prolog license). The ProB constraint solver is implemented using co-routining and the CLP(FD) finite domain library of SICStus. An alternate [[Using_ProB_with_KODKOD | constraint solver based on Kodkod (and thus SAT)]] is also available within ProB, as is an alternate [[TLC|model checking engine (TLC)]] for low-level B specifications. The [[ProBLicence | ProB Licence can be found here]].

== Features ==
ProB covers a [[Summary of B Syntax|large part of B]], and we are striving towards full coverage of Atelier B and B4Free constructs. ProB supports B features such as non-deterministic operations, ANY statements, operations with complex arguments, sets, sequences, functions, lambda abstractions, set comprehensions, records, constants and properties, and many more. Not supported are the Atelier B tree operations and there are restrictions on DEFINITIONS. ProB does support multiple machines, refinements, and implementations. ProB can also be used for automated refinement checking and [[LTL Model Checking|LTL model checking]]. It also [[CSP-M|supports almost full CSP-M]] process descriptions (as of version 1.2.7), to be used on their own or to guide B machines for specification and property validation. The state space of the specifications can be [[Graphical Viewer|graphically visualized]].
ProB also supports Z specifications (ProB in this context is sometimes called [[ProZ]]) as well as [[TLA|TLA+ specifications]]. We now also have an online [[ProB Logic Calculator]].

User:Jens Bendisposto

2015-09-18T15:48:52Z

Jens Bendisposto:

[[Formating_Sandbox]]

[[Jens_Bendisposto:Conferences]]

[[Jens_Bendisposto:Model Checkers]]

[[Jens_Bendisposto:ProB 2.0]]

[[DMC]]

[[parB]]

<html>
<iframe id="forum_embed"
src="javascript:void(0)"
scrolling="no"
frameborder="0"
width="900"
height="700">
</iframe>
<script type="text/javascript">
document.getElementById('forum_embed').src =
'https://groups.google.com/forum/embed/?place=forum/prob-users'
+ '&showsearch=true&showpopout=true&showtabs=false'
+ '&parenturl=' + encodeURIComponent(window.location.href);
</script>
</html>

[https://docs.google.com/document/pub?id=109z3qG6_KBUqm0NC9FaEF1C6_NYCJl453wcXzbovj2Q ProB 2.0 Requirements Document]

{{Bugtrack}}

User:Jens Bendisposto

2015-09-18T15:47:43Z

Jens Bendisposto:

[[Formating_Sandbox]]

[[Jens_Bendisposto:Conferences]]

[[Jens_Bendisposto:Model Checkers]]

[[Jens_Bendisposto:ProB 2.0]]

[[DMC]]

[[parB]]

<html>
<iframe id="forum_embed"
src='https://groups.google.com/forum/embed/?place=forum/prob-users'
+ '&showsearch=true&showpopout=true&showtabs=false&parenturl=http://stups.hhu.de/ProB/w/User:Jens_Bendisposto'
scrolling="no"
frameborder="0"
width="900"
height="700">
</iframe>
</html>

[https://docs.google.com/document/pub?id=109z3qG6_KBUqm0NC9FaEF1C6_NYCJl453wcXzbovj2Q ProB 2.0 Requirements Document]

{{Bugtrack}}

User:Jens Bendisposto

2015-09-18T15:46:25Z

Jens Bendisposto:

[[Formating_Sandbox]]

[[Jens_Bendisposto:Conferences]]

[[Jens_Bendisposto:Model Checkers]]

[[Jens_Bendisposto:ProB 2.0]]

[[DMC]]

[[parB]]

<html>
<iframe id="forum_embed"
src='https://groups.google.com/forum/embed/?place=forum/prob-users'
+ '&showsearch=true&showpopout=true&showtabs=false'
scrolling="no"
frameborder="0"
width="900"
height="700">
</iframe>
</html>

[https://docs.google.com/document/pub?id=109z3qG6_KBUqm0NC9FaEF1C6_NYCJl453wcXzbovj2Q ProB 2.0 Requirements Document]

{{Bugtrack}}

User:Jens Bendisposto

2015-09-18T15:45:15Z

Jens Bendisposto:

ProB Logic Calculator

2015-09-14T10:29:53Z

Jens Bendisposto:

Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial|small tutorial]] at the bottom of the page.

<html>
<iframe src="http://wyvern.cs.uni-duesseldorf.de:8080/evalB/embedded.html" width="780" height="450" border="0" frameborder="0" scrolling="no">
<p>Your Browser does not suport IFrames.</p>
</iframe>
</html>

The above calculator has a time-out of 3 seconds, and <tt>MAXINT</tt> is set to 127 and <tt>MININT</tt> to -128.
A front-end with larger text areas is [http://wyvern.cs.uni-duesseldorf.de:8080/evalB/index.html available here].
An alternative, older version of the calculator is available at the [http://www.formalmind.com/en/blog/prob-logic-calculator Formal Mind website].
You can also [[Download|download ProB]] for execution on your computer, along with support for [http://en.wikipedia.org/wiki/B B], [http://www.event-b.org/ Event-B], [http://en.wikipedia.org/wiki/Communicating_sequential_processes CSP-M],
[http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+], and [http://en.wikipedia.org/wiki/Z_notation Z]. There are also 64-bit versions available for Linux and Mac (the above calculator only uses the 32-bit version).

Short syntax guide for some of B's constructs:
* comments <tt>/* ... */</tt>
* conjunction <tt>P & Q</tt>, disjunction <tt>P or Q</tt>, implication <tt>P => Q</tt>, equivalence <tt>P <=> Q</tt>, negation <tt>not(P)</tt>, existential quantification <tt>#x.(P)</tt>, universal quantification <tt>!x.(P=>Q)</tt>
* equality <tt>x=y</tt>, disequality <tt>x/=y</tt>
* boolean values <tt>TRUE</tt>, <tt>FALSE</tt>, converting predicate to value <tt>bool(P)</tt>; Warning: <tt>TRUE</tt> and <tt>FALSE</tt> are values and <em>not</em> predicates in B and cannot be combined using logical connectives.
* strings <tt>"..."</tt>, set of all strings <tt>STRING</tt>
* arithmetic comparisons <tt>x < y</tt>, <tt>x > y</tt>, <tt>x <= y</tt>, <tt>x >= y</tt>
* membership <tt>x:S</tt>, not membership, <tt>x/:S</tt>, subset <tt>S<:R</tt>, strict subset <tt>S <<: R</tt>
* arithmetic operators <tt>x+y</tt>, <tt>x-y</tt>, <tt>x*y</tt>, <tt>x/y</tt>, <tt>x mod y</tt>, <tt>x**y</tt> , <tt>succ(x)</tt>, <tt>pred(x)</tt>
* mathematical integers <tt>INTEGER</tt>, mathematical natural numbers <tt>NATURAL</tt>, implementable integers <tt>INT</tt>, implementable naturals <tt>NAT</tt>, maximum implementable integer <tt>MAXINT</tt>, minimum implementable integer <tt>MININT</tt>
* empty set <tt>{}</tt>, set enumeration <tt>{x,y,...}</tt>, comprehension set defined by predicate <tt>{x|P}</tt>, lambda abstraction <tt>%x.(P|E)</tt>, interval <tt>m..n</tt>
* set union <tt>S \/ T</tt>, set intersection <tt>S /\ T</tt>, set difference <tt>S - T</tt>, power set <tt>POW(S)</tt>, Cartesian product <tt>S*T</tt>, cardinality of set <tt>card(S)</tt>
* set of relations between two sets <tt>S <-> T</tt>, set of partial functions <tt>S +-> T</tt>, set of total functions <tt>S --> T</tt>
* relational image <tt>r[S]</tt>, relational composition <tt>(r1 ; r2)</tt>, transitive closure <tt>closure1(r)</tt>, identity relation over a set <tt>id(S)</tt>, domain of a relation <tt>dom(r)</tt>, its range <tt>ran(r)</tt>, its inverse <tt>r~</tt>, relational overriding <tt>r1 <+ r2</tt>
* empty sequence <tt>[]</tt>, explicit sequence <tt>[x,y,...]</tt>, concatenation <tt>s1^s2</tt>, first element <tt>first(s)</tt>, tail <tt>tail(s)</tt>, prepend an element <tt>E->s</tt>, size of a sequence <tt>size(s)</tt>
* sets of sequences over a set <tt>seq(S)</tt>, set of injective sequences <tt>iseq(S)</tt>, set of permutations <tt>perm(S)</tt>
More details can be found on our [[Summary_of_B_Syntax|page on the B syntax]]. Note: statements (aka substitutions) and B machine construction elements cannot be used above; you must enter either a predicate or an expression.

The term <em>logic calculator</em> is taken over from [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html Leslie Lamport].
An early implementation of a logic calculator is the [http://en.wikipedia.org/wiki/William_Stanley_Jevons#Logic Logic Piano].

We are grateful for feedback about our logic calculator (send an email to [http://www.stups.uni-duesseldorf.de/~leuschel Michael Leuschel]).
You can also switch the calculator into [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] mode.
In future we plan to provide additional features:
* getting an unsat core for unsatisfiable formulas
* better feedback for syntax and type errors
* graphical visualization of formulas and models
* support for further alternative input syntax, such as [http://en.wikipedia.org/wiki/Z_notation Z]
* ability to change the parameters, e.g., use the [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 ProB-Kodkod backend] instead of the default constraint-logic programming kernel.

== Small Tutorial ==

Here is a small tutorial to get you started.
B distinguishes <em>expressions</em>, which have a value, and <em>predicates</em> which can be either true or false.
First, let us type an expression:
1+1
The calculator returns the value <tt>2</tt>.
A more complicated expression is:
{1,2,3} \/ {1+2+3}
which has the value <tt>{1,2,3,6}</tt>.
Now, let us type a simple predicate:
1>2
The calculator tells us that this predicate is false.
We can combine predicates using the logical connectives.
For example, the following predicate is true:
1>2 or 2>1
We can also use existential quantification to produce a predicate:
#(x).(x+10=30)
which is true and ProB will give you a solution <tt>x=20</tt>.
In the calculator, any variable that is not explicitly introduced is considered existentially quantified. Thus, you get the same effect by simply typing:
x+10=30
If you want to get all solutions for the equation x+10=30, you can make use of a set comprehension:
{x|x+10=30}
Here the calculator will compute the value of the expression to be <tt>{20}</tt>, i.e., we know that 20 is the only solution for <tt>x</tt>.
Note that the B language has Boolean values <tt>TRUE</tt> and <tt>FALSE</tt>, but these are <em>not</em> considered predicates in B.
Thus if we type:
TRUE
this is considered an expression and not a predicate.
This also means that <tt>TRUE or FALSE</tt> is not considered a legal predicate in pure B.
However, for convenience, the logic calculator accepts this and as such you can type:
TRUE or FALSE
which is determined to be true.
In pure B, you would have to write something like:
1=1 or 1=2
Finally, in pure B, variables can only range over values in B, not over predicates. Thus <tt>P or Q</tt> is not allowed in pure B, but our logic calculator does accept it.
As such you can type
P or Q
which is equivalent to typing
P=TRUE or Q=TRUE
If you want to find all models of the formula, you can use a set comprehension:
{P,Q | P or Q}
Also, if you want to check whether your formula is a tautology you can select the "Universal (Checking)" entry in the Quantification Mode menu. In this case (for <tt>P or Q</tt>) a counter example is produced by the tool.
More generally, you can check proof rules using the "Tautology Check" button.
E.g., our tool will confirm that the following is a tautology:
(A => B) & not(B) => not(A)
Note, however, that our tool is <em>not</em> a prover in general: you can use it to find solutions and counter-examples, but in general it cannot be used to prove formulas using variables with infinite type.
In those cases, you may see enumeration warnings in the output, which means that ProB was only able to check a finite number of values from an infinite set. This could mean that the result displayed is not correct (even though in general solutions and counter-examples tend to be correct; in future we will refine ProB's output to also indicate when the solution/counter-example is still guaranteed to be correct)!

== Executing the Calculator locally ==
You can evaluate formulas on your machine in the same way as the calculator above, by [[Download|downloading ProB]] (ideally a nightly build) and then executing one of the following commands:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE
The above command requires you to put the formula into a file <tt>MYFILE</tt>.
The command below allows you to put the formula directly into the command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval "MYFORMULA"
If you want to perform the tautology check you have to do the following using the -eval_rule_file command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE
You can also start your own REPL using the -repl command (you may wish to use the rlwrap tool):
./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128
You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...) according to your needs; the [[Using_the_Command-Line_Version_of_ProB|user manual]] provides more details.
You may wish to use the rlwrap tool:
rlwrap ./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128

Probably, you may want to generate full-fledged B machines as input to <tt>probcli</tt>.
This allows you to introduce enumerated and deferred sets; compared to using sets of strings, this has benefits in terms of more stringent typechecking and more efficient constraint solving.

An alternate front-end to the calculator is [http://wyvern.cs.uni-duesseldorf.de:8080/evalB/ available here].
Its code is available at <tt>https://github.com/bendisposto/evalB</tt>.

ProB Logic Calculator

2015-09-14T10:28:52Z

Jens Bendisposto:

Below is a ProB-based [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html logic calculator]. You can enter predicates and expressions in the upper textfield ([[Summary_of_B_Syntax|using B syntax]]). When you stop typing, ProB will evaluate the formula and display the result in the lower textfield. A series of examples for the "Evaluate" mode can be loaded from the examples menu. There is a [[ProB_Logic_Calculator#Small_Tutorial|small tutorial]] at the bottom of the page.

<html>

</html>

<html>
<iframe src="http://wyvern.cs.uni-duesseldorf.de:8080/evalB/embedded.html" width="780" height="450" border="0" frameborder="0" scrolling="no">
<p>Your Browser does not suport IFrames.</p>
</iframe>
</html>

The above calculator has a time-out of 3 seconds, and <tt>MAXINT</tt> is set to 127 and <tt>MININT</tt> to -128.
A front-end with larger text areas is [http://wyvern.cs.uni-duesseldorf.de:8080/evalB/index.html available here].
An alternative, older version of the calculator is available at the [http://www.formalmind.com/en/blog/prob-logic-calculator Formal Mind website].
You can also [[Download|download ProB]] for execution on your computer, along with support for [http://en.wikipedia.org/wiki/B B], [http://www.event-b.org/ Event-B], [http://en.wikipedia.org/wiki/Communicating_sequential_processes CSP-M],
[http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+], and [http://en.wikipedia.org/wiki/Z_notation Z]. There are also 64-bit versions available for Linux and Mac (the above calculator only uses the 32-bit version).

Short syntax guide for some of B's constructs:
* comments <tt>/* ... */</tt>
* conjunction <tt>P & Q</tt>, disjunction <tt>P or Q</tt>, implication <tt>P => Q</tt>, equivalence <tt>P <=> Q</tt>, negation <tt>not(P)</tt>, existential quantification <tt>#x.(P)</tt>, universal quantification <tt>!x.(P=>Q)</tt>
* equality <tt>x=y</tt>, disequality <tt>x/=y</tt>
* boolean values <tt>TRUE</tt>, <tt>FALSE</tt>, converting predicate to value <tt>bool(P)</tt>; Warning: <tt>TRUE</tt> and <tt>FALSE</tt> are values and <em>not</em> predicates in B and cannot be combined using logical connectives.
* strings <tt>"..."</tt>, set of all strings <tt>STRING</tt>
* arithmetic comparisons <tt>x < y</tt>, <tt>x > y</tt>, <tt>x <= y</tt>, <tt>x >= y</tt>
* membership <tt>x:S</tt>, not membership, <tt>x/:S</tt>, subset <tt>S<:R</tt>, strict subset <tt>S <<: R</tt>
* arithmetic operators <tt>x+y</tt>, <tt>x-y</tt>, <tt>x*y</tt>, <tt>x/y</tt>, <tt>x mod y</tt>, <tt>x**y</tt> , <tt>succ(x)</tt>, <tt>pred(x)</tt>
* mathematical integers <tt>INTEGER</tt>, mathematical natural numbers <tt>NATURAL</tt>, implementable integers <tt>INT</tt>, implementable naturals <tt>NAT</tt>, maximum implementable integer <tt>MAXINT</tt>, minimum implementable integer <tt>MININT</tt>
* empty set <tt>{}</tt>, set enumeration <tt>{x,y,...}</tt>, comprehension set defined by predicate <tt>{x|P}</tt>, lambda abstraction <tt>%x.(P|E)</tt>, interval <tt>m..n</tt>
* set union <tt>S \/ T</tt>, set intersection <tt>S /\ T</tt>, set difference <tt>S - T</tt>, power set <tt>POW(S)</tt>, Cartesian product <tt>S*T</tt>, cardinality of set <tt>card(S)</tt>
* set of relations between two sets <tt>S <-> T</tt>, set of partial functions <tt>S +-> T</tt>, set of total functions <tt>S --> T</tt>
* relational image <tt>r[S]</tt>, relational composition <tt>(r1 ; r2)</tt>, transitive closure <tt>closure1(r)</tt>, identity relation over a set <tt>id(S)</tt>, domain of a relation <tt>dom(r)</tt>, its range <tt>ran(r)</tt>, its inverse <tt>r~</tt>, relational overriding <tt>r1 <+ r2</tt>
* empty sequence <tt>[]</tt>, explicit sequence <tt>[x,y,...]</tt>, concatenation <tt>s1^s2</tt>, first element <tt>first(s)</tt>, tail <tt>tail(s)</tt>, prepend an element <tt>E->s</tt>, size of a sequence <tt>size(s)</tt>
* sets of sequences over a set <tt>seq(S)</tt>, set of injective sequences <tt>iseq(S)</tt>, set of permutations <tt>perm(S)</tt>
More details can be found on our [[Summary_of_B_Syntax|page on the B syntax]]. Note: statements (aka substitutions) and B machine construction elements cannot be used above; you must enter either a predicate or an expression.

The term <em>logic calculator</em> is taken over from [http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html Leslie Lamport].
An early implementation of a logic calculator is the [http://en.wikipedia.org/wiki/William_Stanley_Jevons#Logic Logic Piano].

We are grateful for feedback about our logic calculator (send an email to [http://www.stups.uni-duesseldorf.de/~leuschel Michael Leuschel]).
You can also switch the calculator into [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] mode.
In future we plan to provide additional features:
* getting an unsat core for unsatisfiable formulas
* better feedback for syntax and type errors
* graphical visualization of formulas and models
* support for further alternative input syntax, such as [http://en.wikipedia.org/wiki/Z_notation Z]
* ability to change the parameters, e.g., use the [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 ProB-Kodkod backend] instead of the default constraint-logic programming kernel.

== Small Tutorial ==

Here is a small tutorial to get you started.
B distinguishes <em>expressions</em>, which have a value, and <em>predicates</em> which can be either true or false.
First, let us type an expression:
1+1
The calculator returns the value <tt>2</tt>.
A more complicated expression is:
{1,2,3} \/ {1+2+3}
which has the value <tt>{1,2,3,6}</tt>.
Now, let us type a simple predicate:
1>2
The calculator tells us that this predicate is false.
We can combine predicates using the logical connectives.
For example, the following predicate is true:
1>2 or 2>1
We can also use existential quantification to produce a predicate:
#(x).(x+10=30)
which is true and ProB will give you a solution <tt>x=20</tt>.
In the calculator, any variable that is not explicitly introduced is considered existentially quantified. Thus, you get the same effect by simply typing:
x+10=30
If you want to get all solutions for the equation x+10=30, you can make use of a set comprehension:
{x|x+10=30}
Here the calculator will compute the value of the expression to be <tt>{20}</tt>, i.e., we know that 20 is the only solution for <tt>x</tt>.
Note that the B language has Boolean values <tt>TRUE</tt> and <tt>FALSE</tt>, but these are <em>not</em> considered predicates in B.
Thus if we type:
TRUE
this is considered an expression and not a predicate.
This also means that <tt>TRUE or FALSE</tt> is not considered a legal predicate in pure B.
However, for convenience, the logic calculator accepts this and as such you can type:
TRUE or FALSE
which is determined to be true.
In pure B, you would have to write something like:
1=1 or 1=2
Finally, in pure B, variables can only range over values in B, not over predicates. Thus <tt>P or Q</tt> is not allowed in pure B, but our logic calculator does accept it.
As such you can type
P or Q
which is equivalent to typing
P=TRUE or Q=TRUE
If you want to find all models of the formula, you can use a set comprehension:
{P,Q | P or Q}
Also, if you want to check whether your formula is a tautology you can select the "Universal (Checking)" entry in the Quantification Mode menu. In this case (for <tt>P or Q</tt>) a counter example is produced by the tool.
More generally, you can check proof rules using the "Tautology Check" button.
E.g., our tool will confirm that the following is a tautology:
(A => B) & not(B) => not(A)
Note, however, that our tool is <em>not</em> a prover in general: you can use it to find solutions and counter-examples, but in general it cannot be used to prove formulas using variables with infinite type.
In those cases, you may see enumeration warnings in the output, which means that ProB was only able to check a finite number of values from an infinite set. This could mean that the result displayed is not correct (even though in general solutions and counter-examples tend to be correct; in future we will refine ProB's output to also indicate when the solution/counter-example is still guaranteed to be correct)!

== Executing the Calculator locally ==
You can evaluate formulas on your machine in the same way as the calculator above, by [[Download|downloading ProB]] (ideally a nightly build) and then executing one of the following commands:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE
The above command requires you to put the formula into a file <tt>MYFILE</tt>.
The command below allows you to put the formula directly into the command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval "MYFORMULA"
If you want to perform the tautology check you have to do the following using the -eval_rule_file command:
./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE
You can also start your own REPL using the -repl command (you may wish to use the rlwrap tool):
./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128
You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...) according to your needs; the [[Using_the_Command-Line_Version_of_ProB|user manual]] provides more details.
You may wish to use the rlwrap tool:
rlwrap ./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128

Probably, you may want to generate full-fledged B machines as input to <tt>probcli</tt>.
This allows you to introduce enumerated and deferred sets; compared to using sets of strings, this has benefits in terms of more stringent typechecking and more efficient constraint solving.

An alternate front-end to the calculator is [http://cobra.cs.uni-duesseldorf.de/evalB/ available here].
Its code is available at <tt>https://github.com/bendisposto/evalB</tt>.

2015-03-18T12:14:04Z

Jens Bendisposto:

This page explains how to run the distributed model checking prototype.

Note that the implementation does not work with Windows, only Linux andMac OS are supported.

It is required to set the limits for shared memory on some systems, this can be done using sysctl. Here is a little script that sets the limits. It takes the size of shared memory as parameter (usually the size of your memory in GB). You need to run the script with root rights.

#!/bin/bash
if [ $# -gt 0 ]; then
echo "Setting SHM sizes:"
sysctl -w kern.sysv.shmmax=`perl -e "print 1073741824*$1"`
sysctl -w kern.sysv.shmseg=4096
sysctl -w kern.sysv.shmall=`perl -e "print 262144*$1"`
echo "Here are the current values:"
sysctl -a | grep shm
else
echo "You need to provide the size of shared memort (in full GB)"
fi

After setting up shared memory, you can use the <tt>parB.sh</tt> script that comes with the ProB distribution (see [[Download]]).

Usage
./parB <Nr. of workers> <logfile> <file>

Example usage:
$ ./parB.sh 2 ~/parB.log scheduler.mch

== Running in the Cloud/Cluster ==
The script can only be used for computation on a single physical computer. If you want to use multiple computers, the setup is a bit more complex:

* On each physical computer you need to start exactly one copy of <tt>lib/hasher</tt>.
* Multiple Copies of <tt>probcli</tt> configured as workers:
probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0
* A single instance of <tt>probcli</tt> configured as the master:
probcli -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE>

The minimal queue length is used to determine if a worker is allowed to share its queue. The experiments have shown, that a number between 10 and 100 is fine. parB will stop after (at least) the maximal number of states have been explored, a value of -1 will explore all states (beware of this, if the state space is infinite!).

As a rule of thumb use one real core for each of the processes. On hyperthreads the model checking still becomes faster, but the speedup is only 1/4 for each additional hyperthread.

We plan to develop a control interface that allows configuring the logical network in a more convenient way and running the model checker from within ProB.

== Options ==
You can use preferences in parB.sh (and the master) :
./parB <Nr. of workers> <logfile> <file> <additional probcli options>
./probcli <additional probcli options> -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE> <additional probcli options>

If you use -strict, parB will stop as soon as a violation is found, otherwise parB will explore the full state space (up to the maximal number of states)

== Cleaning up ==
If something goes wrong it may be necessary to clean up your shared memory.
You can find out if there are still memory blocks occupied using <tt>ipcs</tt>.
Removal can be done using:
ipcrm -M `ipcs | grep <YOUR USERNAME> | grep -o "0x[^ ]*" | sed ':a;N;$!ba;s/\n/ -M /g'`

DMC

2015-03-18T10:41:14Z

Jens Bendisposto:

{{DISPLAYTITLE:Distributed Model Checking : Experimental evaluation}}

This page explains the methodology of the experiments carried out to evaluate the distributed version of ProB.

ParB

2015-03-18T10:31:08Z

Jens Bendisposto:

This page explains how to run the distributed model checking prototype.

Note that the implementation does not work with Windows, only Linux andMac OS are supported.

It is required to set the limits for shared memory on some systems, this can be done using sysctl. Here is a little script that sets the limits. It takes the size of shared memory as parameter (usually the size of your memory in GB). You need to run the script with root rights.

#!/bin/bash
if [ $# -gt 0 ]; then
echo "Setting SHM sizes:"
sysctl -w kern.sysv.shmmax=`perl -e "print 1073741824*$1"`
sysctl -w kern.sysv.shmseg=4096
sysctl -w kern.sysv.shmall=`perl -e "print 262144*$1"`
echo "Here are the current values:"
sysctl -a | grep shm
else
echo "You need to provide the size of shared memort (in full GB)"
fi

After setting up shared memory, you can use the <tt>parB.sh</tt> script that comes with the ProB distribution (see [[Download]]).

Usage
./parB <Nr. of workers> <logfile> <file>

Example usage:
$ ./parB.sh 2 ~/parB.log scheduler.mch

== Running in the Cloud/Cluster ==
The script can only be used for computation on a single physical computer. If you want to use multiple computers, the setup is a bit more complex:

* On each physical computer you need to start exactly one copy of <tt>lib/hasher</tt>.
* Multiple Copies of <tt>probcli</tt> configured as workers:
probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0
* A single instance of <tt>probcli</tt> configured as the master:
probcli -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE>

As a rule of thumb use one real core for each of the processes. On hyperthreads the model checking still becomes faster, but the speedup is only 1/4 for each additional hyperthread.

We plan to develop a control interface that allows configuring the logical network in a more convenient way and running the model checker from within ProB.

== Cleaning up ==
If something goes wrong it may be necessary to clean up your shared memory.
You can find out if there are still memory blocks occupied using <tt>ipcs</tt>.
Removal can be done using:
ipcrm -M `ipcs | grep <YOUR USERNAME> | grep -o "0x[^ ]*" | sed ':a;N;$!ba;s/\n/ -M /g'`

ParB

2015-03-18T10:27:13Z

Jens Bendisposto:

ParB

2015-03-18T10:20:55Z

Jens Bendisposto:

ParB

2015-03-16T17:34:50Z

Jens Bendisposto: Created page with 'This page explains how to run the distributed model checking Prototype.'

This page explains how to run the distributed model checking Prototype.

User:Jens Bendisposto

2015-03-16T17:34:07Z

Jens Bendisposto:

[[Formating_Sandbox]]

[[Jens_Bendisposto:Conferences]]

[[Jens_Bendisposto:Model Checkers]]

[[Jens_Bendisposto:ProB 2.0]]

[[DMC]]

[[parB]]

[https://docs.google.com/document/pub?id=109z3qG6_KBUqm0NC9FaEF1C6_NYCJl453wcXzbovj2Q ProB 2.0 Requirements Document]

{{Bugtrack}}

DMC

2015-03-16T17:32:26Z

Jens Bendisposto: Created page with 'This page explains the methodology of the experiments carried out to evaluate the distributed version of ProB.'

This page explains the methodology of the experiments carried out to evaluate the distributed version of ProB.

User:Jens Bendisposto

2015-03-16T17:31:19Z

Jens Bendisposto:

[[Formating_Sandbox]]

[[Jens_Bendisposto:Conferences]]

[[Jens_Bendisposto:Model Checkers]]

[[Jens_Bendisposto:ProB 2.0]]

[[DMC]]

[[Using parB]]

[https://docs.google.com/document/pub?id=109z3qG6_KBUqm0NC9FaEF1C6_NYCJl453wcXzbovj2Q ProB 2.0 Requirements Document]

{{Bugtrack}}

User:Jens Bendisposto

2015-03-16T11:14:05Z

Jens Bendisposto:

[[Formating_Sandbox]]

[[Jens_Bendisposto:Conferences]]

[[Jens_Bendisposto:Model Checkers]]

[[Jens_Bendisposto:ProB 2.0]]

[[Directed and Distributed Model Checking]]

[[Using parB]]

[https://docs.google.com/document/pub?id=109z3qG6_KBUqm0NC9FaEF1C6_NYCJl453wcXzbovj2Q ProB 2.0 Requirements Document]

{{Bugtrack}}