Skip to content
Snippets Groups Projects
Commit 9ed9546a authored by dgelessus's avatar dgelessus
Browse files

Remove unused "obsolete" directory 

They are not included in the handbook. These pages can still be found
on the wiki (and in the Git history).
parent 85a4d60d
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
src/docs/obsolete/ProB_Logic_Calculator_old.adoc deleted 100644 → 0
+ 0
− 257
View file @ 85a4d60d
[[prob-logic-calculator]]
= ProB Logic Calculator
WARNING: This section is relatively old and may contain errors.
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
window (<<summary-of-b-syntax,using B syntax>>), and then press the
"Evaluate" button to ask ProB to evaluate the formula. Variables are
assumed to be implicitly existentially quantified for the "Evaluate"
button which tries to find solutions and universally quantified for the
"Tautology Check" button which tries to find counter-examples. 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.
http://wyvern.cs.uni-duesseldorf.de:8443/index.html[*Click here to get to the ProB Logic Calculator*]
The calculator above has a time-out of 3 seconds, and `MAXINT` is set
to 127 and `MININT` to -128. An alternative version of the calculator is
available at the
http://www.formalmind.com/en/blog/prob-logic-calculator[Formal Mind
website]. You can also <<downloads,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-b-constructs]]
== 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 <<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 logic calculator we use is taken 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 https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/unser-team.html[Michael Leuschel]). 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 alternative input syntax, such as
http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+]
or http://en.wikipedia.org/wiki/Z_notation[Z]
* ability to change the parameters, e.g., use the
https://www3.hhu.de/stups/downloads/pdf/PlaggeLeuschel_Kodkod2012.pdf[ProB-Kodkod
backend] instead of the default constraint-logic programming kernel.
[[small-tutorial]]
== 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, 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
press the "Tautology Check" button. 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]]
== Executing the Calculator locally
You can evaluate formulas on your machine in the same way as the
calculator above, by <<downloads,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:
....
./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 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.
....
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 web interface is currently being developed
http://cobra.cs.uni-duesseldorf.de/evalB/[here]. Its code is available
at
https://github.com/bendisposto/evalB[`https://github.com/bendisposto/evalB`]
and it can easily be run locally using `gradle jWR`.
src/docs/obsolete/Tutorial_Unit_Plugin.adoc deleted 100644 → 0
+ 0
− 114
View file @ 85a4d60d
[[tutorial-unit-plugin]]
= Tutorial Unit Plugin
Note: This feature is no longer available in ProB 1.9.0.
This tutorial describes, how ProB's integrated plugin for unit analysis
can be used to verify the usage of physical units throughout a B
machine. This includes
1. Annotating variables with their physical unit,
2. Infer the unit of variables without an annotation,
3. Detect incorrect usage of units, like addition of differently
annotated variables.
The plugin is currently a work in progress. Rough edges are to be
expected.
We assume that you have a general understanding of B and the usage of
ProB.
[[activating-the-plugin-and-setting-preferences]]
== Activating the Plugin and setting preferences
Currently, the plugin can only be used with classical B machines.
Therefore, a B machine needs to be loaded before the plugin can be
activated.
Once a machine is loaded, the plugin can be activated through ProB's
plugin menu. Choose "Interpreting units stored in pragmas" inside of
the activate plugin submenu. Furthermore, the preferences can be
accessed through the menu.
At this stage, two preferences can be set:
1. Activation or deactivation of a static pre-check, that is run once a
machine is loaded and performs a fix point analysis of the formerly
mentioned usages.
2. The maximal number of iterations that are performed, before the fix
point algorithm stops.
If the static pre-check is activated, the plugin moves the animator into
a fix point state, in which possible unit errors are presented to the
user through ProB's error reporting facilities.
[[annotating-variables-and-animating-a-machine]]
== Annotating variables and animating a machine
To connect a variable with an expected physical unit, a special comment
is placed before the variable.
....
VARIABLES
/*@ unit "10**1 * m**1" */ x
/*@ unit "m**2"*/ y
....
Following the "unit" keyword is a specification of the unit in form of
a B expression. Allowed constructs are multiplication and division as
well as exponentiation.
For several often used units like cm, dm, km, etc. an alias can be used.
....
VARIABLES
/*@ unit "mm" * / x,
/*@ unit "dm" * / y
....
Once at least one variable is annotated, further units can be inferred.
The unit plugin integrates with ProB's animation facilities. Both
results and parameters of operations are displayed with their unit. For
variables, the unit is stored inside the machines state space. This
enables the plugin to be used in conjunction with the evaluation view,
the dot output and most other ProB features.
[[converting-between-units]]
== Converting between units
To distinct between a numerical multiplication, that changes the values
without changing the unit and a multiplication meant to convert between
units, a second pragma is added. To convert between units, add the
respective conversion factor and mark the multiplication as a unit
conversion.
See the following B machine for an example operation:
....
MACHINE SimpleConversion
VARIABLES
/*@ unit "10** -2 *m"*/ xx,
/*@ unit "10** -3 *m"*/ yy,
converted
INVARIANT
xx:NAT &
yy:NAT &
converted:NAT
INITIALISATION xx,yy,converted:=0,0,0
OPERATIONS
n <-- addToXX = n:=xx+1;
mmToCm = converted:=/*@ conversion */(10*yy)
END
....
[[static-analysis]]
== Static analysis
If activated, the results of the static analysis can be accessed from
the plugin menu. Currently, the results include the inferred unit of
every variable inside the active B machine. Furthermore, a warning is
displayed, if multiple units were inferred for a single variable (which
usually is caused by wrong usage of the variable). Another warning
message is shown for variables, for which no unit could be inferred.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment