Alloy: Difference between revisions

No edit summary
No edit summary
Line 40: Line 40:
</pre>
</pre>


is translated to:
This can be loaded in ProB
 
[[File:ProBAlloyQueens.png|400px|center]]
 
 
Internally the Alloy model is translated to the following B model:


<pre>
<pre>

Revision as of 08:24, 7 February 2018


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.

Installation

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

Examples

N-Queens

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

ProBAlloyQueens.png


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