No edit summary |
|||
Line 98: | Line 98: | ||
== Executing the Calculator locally == | == Executing the Calculator locally == | ||
[[file:ProBTerminalizerReplDemo.gif|center||600px]] | |||
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: | 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 | ./probcli -p BOOL_AS_PREDICATE 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 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: | The command below allows you to put the formula directly into the command: | ||
./probcli -p BOOL_AS_PREDICATE | ./probcli -p BOOL_AS_PREDICATE 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: | 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 | ./probcli -p BOOL_AS_PREDICATE 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 | |||
./probcli -repl -p BOOL_AS_PREDICATE | You can also start your own REPL using the -repl command: | ||
./probcli -repl -p BOOL_AS_PREDICATE 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 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: | You may wish to use the rlwrap tool: |
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:
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:
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 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 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 MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE
You can also start your own REPL using the -repl command:
./probcli -repl -p BOOL_AS_PREDICATE 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.
Its code is available at https://github.com/bendisposto/evalB.