No edit summary |
No edit summary |
||
Line 40: | Line 40: | ||
</pre> | </pre> | ||
This can be loaded in ProB | This can be loaded in ProB, as shown in the following screenshot. | ||
To run the "show" command you have to use "Find Sequence..." command in the "Constraint-Based Checking" submenu of the "Verify" menu. | |||
[[File:ProBAlloyQueens.png|400px|center]] | [[File:ProBAlloyQueens.png|400px|center]] | ||
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.
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 in the "Constraint-Based Checking" submenu of the "Verify" menu.
Internally the Alloy model is translated to the following B model:
/*@ generated */ MACHINE queens SETS queen_ CONSTANTS x_queen, x__queen, y_queen DEFINITIONS show_ == 1=1 ; SET_PREF_MAXINT == 15 ; SET_PREF_MININT == -16 PROPERTIES (!(q_, q__).({q_} <: queen_ & {q__} <: (queen_ - {q_}) => (not((x_queen(q_) = x_queen(q__)))) & (not((y_queen(q_) = y_queen(q__)))) & (not(((x_queen(q_) + y_queen(q_)) = (x_queen(q__) + y_queen(q__))))) & (not(((x__queen(q_) + y_queen(q_)) = (x__queen(q__) + y_queen(q__))))))) & card(queen_) = 4 & /* from signature declaration */ !(this_).({this_} <: queen_ => ((x_queen(this_) >= 1)) & ((y_queen(this_) >= 1)) & ((x_queen(this_) <= card(queen_))) & ((y_queen(this_) <= card(queen_))) & ((x__queen(this_) >= 1)) & ((x__queen(this_) <= card(queen_))) & ((x__queen(this_) = ((card(queen_) + 1) - x_queen(this_))))) & x_queen : queen_ --> INT & x__queen : queen_ --> INT & y_queen : queen_ --> INT OPERATIONS run_show = PRE show_ THEN skip END END