Alloy

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

is translated to:

/*@ 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