No edit summary |
(Add updated syntax overview (from prob2-doc, originally added by Joshua Schmidt)) |
||

Line 246: | Line 246: | ||

one DECL | P existential quantification with exactly one solution | one DECL | P existential quantification with exactly one solution | ||

lone DECL | P quantification with one or zero solutions | lone DECL | P quantification with one or zero solutions | ||

where the DECL follow the following form: | where the DECL follow the following form: | ||

x : S choose a singleton subset of S (like x : one S) | x : S choose a singleton subset of S (like x : one S) | ||

x : one S choose a singleton subset of S | x : one S choose a singleton subset of S | ||

Line 264: | Line 264: | ||

S & T set intersection | S & T set intersection | ||

S - T set difference | S - T set difference | ||

# S | # S cardinality of set | ||

Set Predicates: | Set Predicates: | ||

Line 277: | Line 277: | ||

{x:S | P} set comprehension | {x:S | P} set comprehension | ||

{DECL | P} set comprehension, DECL has same format as for quantifiers | {DECL | P} set comprehension, DECL has same format as for quantifiers | ||

let s : S | P | let s : S | P identifier definition | ||

Relation Expressions: | Relation Expressions: | ||

Line 289: | Line 289: | ||

^R transitive closure of binary relation | ^R transitive closure of binary relation | ||

*R reflexive and transitive closure | *R reflexive and transitive closure | ||

Multiplicity Declarations: | Multiplicity Declarations: | ||

--------------------------- | --------------------------- | ||

The following multiplicity annotations are supported for binary (sub)-relations: | The following multiplicity annotations are supported for binary (sub)-relations: | ||

f in S -> T f is any relation from S to T (subset of cartesian product) | f in S -> T f is any relation from S to T (subset of cartesian product) | ||

f in S -> lone T f is a partial function from S to T | f in S -> lone T f is a partial function from S to T | ||

f in S -> one T f is a total function from S to T | f in S -> one T f is a total function from S to T | ||

f in S -> some T f is a total relation from S to T | f in S -> some T f is a total relation from S to T | ||

f in S one -> one T f is a total bijection from S to T | f in S one -> one T f is a total bijection from S to T | ||

f in S lone -> lone T f is a partial injection from S to T | f in S lone -> lone T f is a partial injection from S to T | ||

f in S lone -> one T f is a total injection from S to T | f in S lone -> one T f is a total injection from S to T | ||

f in S some -> lone T f is a partial surjection from S to T | f in S some -> lone T f is a partial surjection from S to T | ||

f in S some -> one T f is a total surjection from S to T | f in S some -> one T f is a total surjection from S to T | ||

f in S some -> T f is a surjective relation from S to T | f in S some -> T f is a surjective relation from S to T | ||

f in S some -> some T f is a total surjective relation from S to T | f in S some -> some T f is a total surjective relation from S to T | ||

Ordered Signatures: | Ordered Signatures: | ||

Line 311: | Line 311: | ||

open util/ordering [S] as s | open util/ordering [S] as s | ||

s/first first element | s/first first element | ||

s/last | s/last last element | ||

s/next[s2] element after s2 | s/max returns the largest element in s or the empty set | ||

s/nexts[s2] all elements after s2 | s/min returns the smallest element in s or the empty set | ||

s/prev[s2] element before s2 | s/next[s2] element after s2 | ||

s/prevs[s2] all elements before s2 | s/nexts[s2] all elements after s2 | ||

s/prev[s2] element before s2 | |||

s/prevs[s2] all elements before s2 | |||

s/smaller[e1,e2] return the element with the smaller index | |||

s/larger[e1,e2] returns the element with the larger index | |||

s/lt[e1,e2] true if index(e1) < index(e2) | |||

s/lte[s2] true if index(e1) =< index(e2) | |||

s/gt[s2] true if index(e1) > index(e2) | |||

s/gte[s2] true if index(e1) >= index(e2) | |||

Sequences: | Sequences: | ||

---------- | ---------- | ||

The longest allowed sequence length (maxseq) is set in the scope of a run or check command using the 'seq' keyword. | |||

Otherwise, a default value is used. | |||

The elements of a sequence s are enumerated from 0 to #s-1. | |||

s : seq S ordered and indexed sequence | |||

#s the cardinality of s | |||

s.isEmpty true if s is empty | |||

s.hasDups true if s contains duplicate elements | |||

s.first head element | |||

s.last last element | |||

s.butlast s without its last element | |||

s.rest tail of the sequence | |||

s.inds the set {0,..,#s-1} if s is not empty, otherwise the empty set | |||

s.lastIdx #s-1 if s is not empty, otherwise the empty set | |||

s.afterLastIdx #s if s is smaller than maxseq, otherwise the empty set | |||

s.idxOf [x] the first index of the occurence of x in s, the empty set if x does not occur in s | |||

s.add[x] insert x at index position i | |||

s.indsOf[i] the set of indices where x occurs in s, the empty set if x does not occur in s | |||

s.delete[i] delete the element at index i | |||

s.lastIdxOf[x] the last index of the occurence of x in s, the empty set if x does not occur in s | |||

s.append[s2] concatenate s and s2, truncate the result if it contains more than maxseq elements | |||

s.insert[i,x] insert x at index position i, remove the last element if #s = maxseq | |||

s.setAt[i,x] replace the value at index position i with x | |||

s.subseq[i,j] the subsequence of s from indices i to j inclusively | |||

[see http://alloy.lcs.mit.edu/alloy/documentation/quickguide/seq.html] | |||

Arithmetic Expressions and Predicates: | Arithmetic Expressions and Predicates: | ||

Line 363: | Line 391: | ||

check NAME | check NAME | ||

run NAME for x | run NAME for x global scope of less or equal x | ||

run NAME for exactly x1 but x2 S | run NAME for exactly x1 but x2 S global scope of x1 but less or equal x2 S | ||

run NAME for x1 S1,...,xk Sk | run NAME for x1 S1,...,xk Sk individual scopes for signatures S1,..,Sk | ||

run NAME for x Int | run NAME for x Int specify the integer bitwidth (integer overflows might occur) | ||

run NAME for x seq specify the longest allowed sequence length | |||

</pre> | </pre> |

As of version 1.8 ProB provides support to load Alloy models.
The Alloy models are translated to B machines by a Java frontend.

This work and web page is still experimental.

The work is based on a translation of the specification language Alloy to classical B. The translation allows us to load Alloy models into ProB in order to find solutions to the model's constraints. The translation is syntax-directed and closely follows the Alloy grammar. Each Alloy construct is translated into a semantically equivalent component of the B language. In addition to basic Alloy constructs, our approach supports integers and orderings.

Alloy2B is included as of version 1.8.2 of ProB.

You can build Alloy2B yourself:

- Clone or download Alloy2B project on Github.
- Make jar file (gradle build) and
- put resulting alloy2b-*.jar file into ProB's lib folder.

module queens open util/integer sig queen { x:Int, x':Int, y:Int } { x >= 1 y >= 1 x <= #queen y <= #queen x' >=1 x' <= #queen x' = minus[plus[#queen,1],x] } fact { all q:queen, q':(queen-q) { ! q.x = q'.x ! q.y = q'.y ! plus[q.x,q.y] = plus[q'.x,q'.y] ! plus[q.x',q.y] = plus[q'.x',q'.y] }} pred show {} run show for exactly 4 queen, 5 int

This can be loaded in ProB, as shown in the following screenshot. To run the "show" command you have to use "Find Sequence..." command for "run_show" in the "Constraint-Based Checking" submenu of the "Verify" menu.

Internally the Alloy model is translated to the following B model:

MACHINE alloytranslation SETS /* deferred */ queen CONCRETE_CONSTANTS x, x_, y /* PROMOTED OPERATIONS run0 */ PROPERTIES x : queen --> INTEGER & x_ : queen --> INTEGER & y : queen --> INTEGER & !this.(this : queen => x(this) >= 1 & y(this) >= 1 & x(this) <= card(queen) & y(this) <= card(queen) & x_(this) >= 1 & x_(this) <= card(queen) & x_(this) = (card(queen) + 1) - x(this) ) & card(queen) = 4 & !(q,q_).(q_ : queen - {q} => not(x(q) = x(q_)) & not(y(q) = y(q_)) & not(x(q) + y(q) = x( q_) + y(q_)) & not(x_(q) + y(q) = x_(q_) + y(q_))) INITIALISATION skip OPERATIONS run0 = PRE card(queen) = 4 & !(q,q_).(q_ : queen - {q} => not(x(q) = x(q_)) & not(y(q) = y(q_)) & not(x(q) + y(q) = x(q_) + y(q_)) & not(x_(q) + y(q) = x_(q_) + y(q_))) THEN skip END /* DEFINITIONS PREDICATE show; */ END

module river_crossing open util/ordering[State] abstract sig Object { eats: set Object } one sig Farmer, Fox, Chicken, Grain extends Object {} fact { eats = Fox->Chicken + Chicken->Grain} sig State { near, far: set Object } fact { first.near = Object && no first.far } pred crossRiver [from, from', to, to': set Object] { one x: from | { from' = from - x - Farmer - from'.eats to' = to + x + Farmer } } fact { all s: State, s': s.next { Farmer in s.near => crossRiver [s.near, s'.near, s.far, s'.far] else crossRiver [s.far, s'.far, s.near, s'.near] } } run { last.far=Object } for exactly 8 State

This can be loaded in ProB, as shown in the following screenshot. To run the "show" command you have to use "Find Sequence..." command for "run_show" in the "Constraint-Based Checking" submenu of the "Verify" menu (after enabling Kodkod in the Preferences menu).

Internally the Alloy model is translated to the following B model:

/*@ generated */ MACHINE river_crossing SETS Object_ CONSTANTS Farmer_, Fox_, Chicken_, Grain_, eats_Object, near_State, far_State DEFINITIONS crossRiver_(from_,from__,to_,to__) == from_ <: Object_ & from__ <: Object_ & to_ <: Object_ & to__ <: Object_ & (card({x_ | {x_} <: from_ & (((from__ = (((from_ - {x_}) - {Farmer_}) - eats_Object[from__]))) & ((to__ = ((to_ \/ {x_}) \/ {Farmer_}))))}) = 1) ; next_State_(s) == {x|x=s+1 & x:State_} ; nexts_State_(s) == {x|x>s & x:State_} ; prev_State_(s) == {x|x=s-1 & x:State_} ; prevs_State_(s) == {x|x<s & x:State_} ; State_ == 0..7 PROPERTIES {Farmer_} <: Object_ & {Fox_} <: Object_ & {Chicken_} <: Object_ & {Grain_} <: Object_ & ((eats_Object = (({Fox_} * {Chicken_}) \/ ({Chicken_} * {Grain_})))) & (((near_State[{min(State_)}] = Object_) & far_State[{min(State_)}] = {})) & (!(s_, s__).({s_} <: State_ & {s__} <: next_State_(s_) => ((({Farmer_} <: near_State[{s_}]) => crossRiver_(near_State[{s_}], near_State[{s__}], far_State[{s_}], far_State[{s__}])) & (not(({Farmer_} <: near_State[{s_}])) => crossRiver_(far_State[{s_}], far_State[{s__}], near_State[{s_}], near_State[{s__}]))))) & Farmer_ /= Fox_ & Farmer_ /= Chicken_ & Farmer_ /= Grain_ & Fox_ /= Chicken_ & Fox_ /= Grain_ & Chicken_ /= Grain_ & {Farmer_} \/ {Fox_} \/ {Chicken_} \/ {Grain_} = Object_ & eats_Object : Object_ <-> Object_ & near_State : State_ <-> Object_ & far_State : State_ <-> Object_ OPERATIONS run_2 = PRE (far_State[{max(State_)}] = Object_) THEN skip END END

sig Object {} sig Vars { src,dst : Object } pred move (v, v': Vars, n: Object) { v.src+v.dst = Object n in v.src v'.src = v.src - n v'.dst = v.dst + n } assert add_preserves_inv { all v, v': Vars, n: Object | move [v,v',n] implies v'.src+v'.dst = Object } check add_preserves_inv for 3

Note that our translation does not (yet) generate an idiomatic B encoding, with `move` as B operation

andsrc+dst=Objectas invariant: it generates a check operation encoding the predicateadd_preserves_invwith universal quantification.

Below we shoe the B machine we have input into AtelierB. It was obtained by pretty-printing from \prob, and putting the negated guard

of theadd_preserves_invinto an assertion (so that AtelierB generates the desired proof obligation).

MACHINE alloytranslation SETS /* deferred */ Object_; Vars_ CONCRETE_CONSTANTS src_Vars, dst_Vars PROPERTIES src_Vars : Vars_ --> Object_ & dst_Vars : Vars_ --> Object_ ASSERTIONS !(v_,v__,n_).(v_ : Vars_ & v__ : Vars_ & n_ : Object_ => (src_Vars[{v_}] \/ dst_Vars[{v_}] = Object_ & v_ |-> n_ : src_Vars & src_Vars[{v__}] = src_Vars[{v_}] - {n_} & dst_Vars[{v__}] = dst_Vars[{v_}] \/ {n_} => src_Vars[{v__}] \/ dst_Vars[{v__}] = Object_) ) END

The following shows AtelierB proving the above assertion:

Logical predicates: ------------------- P and Q conjunction P or Q disjunction P implies Q implication P iff Q equivalence not P negation Alternative syntax: P && Q conjunction P || Q disjunction P => Q implication P <=> Q equivalence ! P negation Quantifiers: ------------- all DECL | P universal quantification some DECL | P existential quantification one DECL | P existential quantification with exactly one solution lone DECL | P quantification with one or zero solutions where the DECL follow the following form: x : S choose a singleton subset of S (like x : one S) x : one S choose a singleton subset of S x : S choose x to be any subset of S x : some S choose x to be any non-empty subset of S x : lone S choose x to be empty or a singleton subset of S x : Rel where Rel is a cartesian product / relation: see multiplicity declarations x in Rel x,y... : S, v,w,... : T means x:S and y : S and ... v:T and w:T and ... disjoint x,y,... : S means x : S and y : S and ... and x,y,... are all pairwise distinct Set Expressions: ---------------- univ all objects none empty set S + T set union S & T set intersection S - T set difference # S cardinality of set Set Predicates: --------------- no S set S is empty S in T R is subset of S S = T set equality S != T set inequality some S set S is not empty one S S is singleton set lone S S is empty or a singleton {x:S | P} set comprehension {DECL | P} set comprehension, DECL has same format as for quantifiers let s : S | P identifier definition Relation Expressions: ---------------------- R -> S Cartesian product R . S relational join S <: R domain restriction of relation R for unary set S R :> S range restriction of relation R for unary set S R ++ Q override of relation R by relation Q ~R relational inverse ^R transitive closure of binary relation *R reflexive and transitive closure Multiplicity Declarations: --------------------------- The following multiplicity annotations are supported for binary (sub)-relations: f in S -> T f is any relation from S to T (subset of cartesian product) f in S -> lone T f is a partial function from S to T f in S -> one T f is a total function from S to T f in S -> some T f is a total relation from S to T f in S one -> one T f is a total bijection from S to T f in S lone -> lone T f is a partial injection from S to T f in S lone -> one T f is a total injection from S to T f in S some -> lone T f is a partial surjection from S to T f in S some -> one T f is a total surjection from S to T f in S some -> T f is a surjective relation from S to T f in S some -> some T f is a total surjective relation from S to T Ordered Signatures: ------------------- A signature S can be defined to be ordered: open util/ordering [S] as s s/first first element s/last last element s/max returns the largest element in s or the empty set s/min returns the smallest element in s or the empty set s/next[s2] element after s2 s/nexts[s2] all elements after s2 s/prev[s2] element before s2 s/prevs[s2] all elements before s2 s/smaller[e1,e2] return the element with the smaller index s/larger[e1,e2] returns the element with the larger index s/lt[e1,e2] true if index(e1) < index(e2) s/lte[s2] true if index(e1) =< index(e2) s/gt[s2] true if index(e1) > index(e2) s/gte[s2] true if index(e1) >= index(e2) Sequences: ---------- The longest allowed sequence length (maxseq) is set in the scope of a run or check command using the 'seq' keyword. Otherwise, a default value is used. The elements of a sequence s are enumerated from 0 to #s-1. s : seq S ordered and indexed sequence #s the cardinality of s s.isEmpty true if s is empty s.hasDups true if s contains duplicate elements s.first head element s.last last element s.butlast s without its last element s.rest tail of the sequence s.inds the set {0,..,#s-1} if s is not empty, otherwise the empty set s.lastIdx #s-1 if s is not empty, otherwise the empty set s.afterLastIdx #s if s is smaller than maxseq, otherwise the empty set s.idxOf [x] the first index of the occurence of x in s, the empty set if x does not occur in s s.add[x] insert x at index position i s.indsOf[i] the set of indices where x occurs in s, the empty set if x does not occur in s s.delete[i] delete the element at index i s.lastIdxOf[x] the last index of the occurence of x in s, the empty set if x does not occur in s s.append[s2] concatenate s and s2, truncate the result if it contains more than maxseq elements s.insert[i,x] insert x at index position i, remove the last element if #s = maxseq s.setAt[i,x] replace the value at index position i with x s.subseq[i,j] the subsequence of s from indices i to j inclusively [see http://alloy.lcs.mit.edu/alloy/documentation/quickguide/seq.html] Arithmetic Expressions and Predicates: -------------------------------------- You need to open util/integer: plus[X,Y] addition minus[X,Y] subtraction mul[X,Y] multiplication div[X,Y] division rem[X,Y] remainder sum[S] sum of integers of set S X < Y less X = Y integer equality X != Y integer inequality X > Y greater X =< Y less or equal X >= Y greater or equal Structuring: ------------ fact NAME { PRED } fact NAME (x1,...,xk : Set) { PRED } pred NAME { PRED } pred NAME (x1,...,xk : Set) { PRED } assert NAME { PRED } fun NAME : Type { EXPR } Commands: --------- run NAME check NAME run NAME for x global scope of less or equal x run NAME for exactly x1 but x2 S global scope of x1 but less or equal x2 S run NAME for x1 S1,...,xk Sk individual scopes for signatures S1,..,Sk run NAME for x Int specify the integer bitwidth (integer overflows might occur) run NAME for x seq specify the longest allowed sequence length