Revision as of 08:53, 6 October 2017 by Jens Bendisposto (talk | contribs)

Below is a ProB-based logic calculator. You can enter predicates and expressions in the upper textfield (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 small tutorial at the bottom of the page.

The above calculator has a time-out of 3 seconds, and `MAXINT` is set to 127 and `MININT` to -128.
You can also download ProB for execution on your computer, along with support for B, Event-B, CSP-M,
TLA+, and Z.

Short syntax guide for some of B's constructs:

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

More details can be found on our 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 *logic calculator* is taken over from Leslie Lamport.
An early implementation of a logic calculator is the Logic Piano.

We are grateful for feedback about our logic calculator (send an email to Michael Leuschel). You can also switch the calculator into 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 Z
- ability to change the parameters, e.g., use the ProB-Kodkod backend instead of the default constraint-logic programming kernel.

Here is a small tutorial to get you started.
B distinguishes *expressions*, which have a value, and *predicates* which can be either true or false.
First, let us type an expression:

1+1

The calculator returns the value `2`.
A more complicated expression is:

{1,2,3} \/ {1+2+3}

which has the value `{1,2,3,6}`.
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 `x=20`.
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 `{20}`, i.e., we know that 20 is the only solution for `x`.
Note that the B language has Boolean values `TRUE` and `FALSE`, but these are *not* considered predicates in B.
Thus if we type:

TRUE

this is considered an expression and not a predicate.
This also means that `TRUE or FALSE` 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 `P or Q` 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 `P or Q`) 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 *not* 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)!

You can evaluate formulas on your machine in the same way as the calculator above, by 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 `MYFILE`.
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 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 `probcli`.
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 available here.
Its code is available at `https://github.com/bendisposto/evalB`.