ProB Logic Calculator: Difference between revisions

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. A front-end with larger text areas is available here. An alternative, older version of the calculator is available at the Formal Mind website. You can also download ProB for execution on your computer, along with support for B, Event-B, CSP-M, TLA+, and 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 /* ... */
• 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.

Small Tutorial

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)!

Executing the Calculator locally

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 and it can easily be run locally using gradle jWR. The old version of the ProB Logic Calculator is still available.