• Special Pages
• User

# Difference between revisions of "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
```

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
```