αRby—An Embedding of Alloy in Ruby

about αRby

• declarative modeling language embedded in an imperative programming language
• beneficial to both the modeling community of Alloy and the object-oriented community of Ruby programmers
• benefits to Alloy users:
  • mixed execution
  • partial instances
  • staged model finding
• benefits to Ruby users:
  • seamless embedding of a relational constraint solver

download & run

download

arby @ github

license

GPLv3

requirements

Ruby 1.9.3 or higher (not tested with 2.1.1) and JDK 1.6 or higher (not tested with 1.8)

  export JAVA_HOME="/etc/java-6-openjdk" ## or wherever your Java is installed
  git clone https://github.com/sdg-mit/arby.git
  cd arby
  bundle install
  ./run_tests.sh test/unit/arby/models/abz14/sudoku_test.rb ## runs a given test only
  ./run_tests.sh ## runs all tests

publications/documentation

• αRby—An Embedding of Alloy in Ruby [slides] [abstract] [full text] [bibtex]
  A. Milicevic, Ido Efrati, and D. Jackson
  International Conference of Alloy, ASM, B, VDM, and Z Users (ABZ 2014), Toulouse, France, June 2014.
  

sample models

examples

hamiltonian path

alloy :GraphModel do
 sig Node [val: (lone Int)]
 sig Edge [src, dst: (one Node)] {src != dst}
 sig Graph[nodes:(set Node), edges:(set Edge)]

 pred hampath[g: Graph, path: (seq Node)] {
  path[Int] == g.nodes and
  path.size == g.nodes.size and
  all(i: 0...path.size-1) | 
   some(e: g.edges) { 
    e.src == path[i] && e.dst == path[i+1] }
 }
 assertion reach {
  all(g: Graph, path: (seq Node)) |
   if hampath(g, path)
    g.nodes.in? path[0].*((~src).dst)
   end }
 run :hampath, 5, Graph=>exactly(1), Node=>3
 check :reach, 5, Graph=>exactly(1), Node=>3
 end

module GraphModel
sig Node {val: lone Int}
sig Edge {src, dst: one Node}{src != dst}
sig Graph{nodes: set Node, edges: set Edge}

pred hampath[g: Graph, path: seq Node] {
 path[Int] = g.nodes
 #path = #g.nodes
 all i: Int | i >= 0 && i < minus[#path,1] => {
  some e: g.edges | 
   e.src = path[i] && e.dst = path[plus[i,1]] }
 }
 assert reach {
  all g: Graph, path: seq Node |
   hampath[g, path] => 
    g.nodes in path[0].*(~src.dst)
 }
run hampath for 5 but exactly 1 Graph, 3 Node
check reach for 5 but exactly 1 Graph, 3 Node

module GraphModel
 class Node;  attr_accessor :val end
 class Edge;  attr_accessor :src, :dst end
 class Graph; attr_accessor :nodes, :edges end

 def self.hampath(g, path) <same as above> end
 def self.reach()          <same as above> end
 def self.run_hampath() exe_cmd :hampath end
 def self.check_reach() exe_cmd :reach end
 end

# find an instance satisfying the :hampath pred
sol = GraphModel.run_hampath
assert sol.satisfiable?
g, path = sol["$hampath_g"], sol["$hampath_path"]
puts g.nodes # => e.g., {<Node$0>, <Node$1>}
puts g.edges # => e.g., {<Node$1, Node$0>}
puts path    # => {<0, Node$1>, <1, Node$0>}
# check that the "reach" assertion holds
sol = GraphModel.check_reach
assert !sol.satisfiable? 

sudoku

alloy :SudokuModel do
 SudokuModel::N = 9

 sig Sudoku[grid: Int ** Int ** (lone Int)]

 pred solved[s: Sudoku] {
  m   = Integer(Math.sqrt(N))
  rng = lambda{|i| m*i...m*(i+1)}

  all(r: 0...N) { 
   s.grid[r][Int] == (1..N) and 
   s.grid[Int][r] == (1..N) 
  } and
  all(c, r: 0...m) { 
   s.grid[rng[c]][rng[r]] == (1..N) 
  }
 }
 end

class SudokuModel::Sudoku
 def pi
  bnds = Arby::Ast::Bounds.new
  inds = (0...N)**(0...N) - self.grid.project(0..1)
  bnds[Sudoku]         = self
  bnds.lo[Sudoku.grid] = self ** self.grid
  bnds.hi[Sudoku.grid] = self ** inds ** (1..N)
  bnds.bound_int(0..N)
 end
 def solve() SudokuModel.solve :solved, self.pi end
 def display() puts grid end
 def self.parse(s) Sudoku.new grid: 
  s.split(/;\s*/).map{|x| x.split(/,/).map(&:to_i)}
 end
end
SudokuModel.N = 4
s = Sudoku.parse "0,0,1; 0,3,4; 3,1,1; 2,2,3"
s.solve(); s.display(); # => {<0,0,1>,<0,1,3>,...}

def dec(sudoku, order=Array(0...sudoku.grid.size).shuffle)
 return nil if order.empty? # all possibilities exhausted
 s_dec = Sudoku.new grid: sudoku.grid.delete_at(order.first) # delete a tuple at random position
 sol   = s_dec.clone.solve() # clone so that "s_dec" doesn't get updated if a solution is found
 (sol.satisfiable? && !sol.next.satisfiable?) ? s_dec : dec(sudoku, order[1..-1])
end
def min(sudoku) (s1 = dec(sudoku)) ? min(s1) : sudoku end
s = Sudoku.new; s.solve(); s = min(s); puts "local minimum found: #{s.grid.size}"

grammar

main syntactic differences between αRby and Alloy

x = y

x == y

sig S {
  f: lone S -> Int
}

sig S [
  f: lone(S) ** Int
]

fun f[s: S]: set S {}

fun f[s: S][set S] {}

{s: S | p1[s]}

S.select{|s| p1[s]}

all s: S {
  p1[s]
  p2[s]
}

all(s: S) {
  p1(s) and
  p2(s)
}

x in y, x !in y 
x !> y 
x -> y 
x . y 
#x 
x => y 
x => y else z 
S <: f, f >: Int

x.in?(y), x.not_in?(y)
not x > y
x ** y
x.(y)
x.size
y if x
if x then y else z
S.< f, f.> Int

^x
*x

x.closure
x.rclosure

f1[x]

f1(x)

BNF grammar

spec      ::= "alloy" cname "do" [open*] paragraph* "end"
open      ::= "open" cnameID
paragraph ::= factDecl   | funDecl | cmdDecl | sigDecl 
sigQual   ::= "abstract" | "lone"  | "one"   | "some"  | "ordered"
sigDecl   ::= sigQual* "sig"  cname,+ ["extends" cnameID] ["[" rubyHash "]"] [block]
factDecl  ::= "fact"         [fname] block
funDecl   ::= "fun"           fname  "[" rubyHash "]"  "[" expr "]" block
            | "pred"          fname ["[" rubyHash "]"]              block
cmdDecl   ::= ("run"|"check") fname "," scope
            | ("run"|"check") "(" scope ")" block
expr      ::= ID | rubyInt | rubyBool | "(" expr ")"
            | unOp expr         | unMeth "(" expr ")"
            | expr binOp expr   | expr "[" expr "]"    | expr "if" expr
            | expr "." "(" expr ")"                   // relational join
            | expr "." (binMeth | ID) "(" expr,* ")"  // function/predicate call
            | "if" expr "then" expr ["else" expr] "end"
            | quant "(" rubyHash ")" block
quant     ::= "all" | "no" | "some" | "lone" | "one" | "sum" | "let" | "select"
binOp     ::= "||" | "or" | "&&" | "and" | "**" | "&" | "+" | "-" | "*" | "/" | "%" 
            | "<<" | ">>" | "==" | "<=>" | "!=" | "<" | ">" | "<=" | ">="
binMeth   ::= "closure" | "rclosure" | "size" | "in?" | "shr" | "<" | ">" | "*" | "^"
unOp      ::= "!" | "~" | "not" 
unMeth    ::= "no" | "some" | "lone" | "one" | "set" | "seq"
block     ::= "{" stmt* "}" | "do" stmt* "end"
stmt      ::= expr | rubyStmt
scope     ::= rubyInt "," rubyHash  // global scope, individual sig scopes
ID        ::= cnameID | fnameID
cname     ::= cnameID | '"'cnameID'"' | "'"cnameID"'" | ":"cnameID
fname     ::= fnameID | '"'fnameID'"' | "'"fnameID"'" | ":"fnameID
cnameID   ::= ___constant identifier in Ruby (starts with upper case)___
fnameID   ::= ___function identifier in Ruby (starts with lower case)___