test

LICENSE 2

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2019 Brown University, Tim Nelson, and Forge contributors
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

forge/examples/basic/booleanLogic 2.frg

@@ -0,0 +1,65 @@
+#lang forge
+
+/*
+  Rough example boolean-logic model in Forge  
+*/
+
+
+------------------------------------------------------
+-- Formula Type
+------------------------------------------------------
+
+abstract sig Formula {
+  truth: set Instance -- Instances this is true in
+}
+sig Var extends Formula {}
+
+sig Instance {
+  trueVars: set Var
+}
+
+
+sig Not extends Formula {child: one Formula}
+sig And extends Formula {aleft, aright: one Formula}
+sig Or extends Formula {oleft, oright: one Formula}
+
+pred children {
+  all n: Not | n.truth = Instance - n.child.truth
+  all a: And | a.truth = a.aleft.truth & a.aright.truth
+  all o: Or | o.truth = o.oleft.truth + o.oright.truth
+}
+-- IMPORTANT: don't add new formulas without updating allSubformulas and children
+
+------------------------------------------------------
+-- Axioms and helpers
+------------------------------------------------------
+
+fun allSubformulas[f: Formula]: set Formula {
+  f.^(child + oleft + oright + aleft + aright)
+}
+
+pred wellFormed {
+  -- no cycles
+  all f: Formula | f not in allSubformulas[f]
+
+  -- via abstract
+  -- all f: Formula | f in Not + And + Or + Var
+
+  all f: Var | f.truth = {i: Instance | f in i.trueVars}
+}
+
+------------------------------------------------------
+
+--GiveMeAFormula : run {children and wellFormed and some Formula} for 5 Formula, 5 Instance
+
+pred GiveMeABigFormula {
+  children 
+  wellFormed 
+  some f: Formula | {
+    #(allSubformulas[f] & Var) > 2
+    some i: Instance | i not in f.truth
+    some i: Instance | i in f.truth
+  }
+}
+
+nameThisRun : run GiveMeABigFormula for 8 Formula, 2 Instance, 5 Int -- need 2 instances

forge/examples/basic/buckets 2.frg

@@ -0,0 +1,62 @@
+#lang forge/temporal
+
+option max_tracelength 10
+
+/*
+  Water buckets puzzle:
+    - you have a faucet of running water
+    - you have empty 8, 5, and 3-liter buckets 
+    - you must get exactly 4 liters of water into one of the buckets using these tools.
+
+  We'll solve this puzzle with Forge. To do so, we'll define the *transition system* 
+  of the puzzle, and ask Forge to search it for a solution! 
+
+  Note that "find a sequence of operations such that <a state like this> is reached"
+  is useful for software and hardware verification, as well...
+*/
+
+sig Bucket {
+    capacity: one Int,
+    var contents: one Int
+}
+one sig B8, B5, B3 extends Bucket {} 
+
+pred initial {
+    B8.capacity = 8 
+    B5.capacity = 5 
+    B3.capacity = 3
+    B8.contents = 0
+    B5.contents = 0
+    B3.contents = 0
+}
+
+pred fill[b: Bucket] {
+    b.contents' = b.capacity
+    all b2: Bucket - b | b2.contents' = b2.contents
+}
+
+pred empty[b: Bucket] {
+    b.contents' = 0
+    all b2: Bucket - b | b2.contents' = b2.contents
+}
+
+pred pour[from, to: Bucket] {
+    let moved = min[from.contents + subtract[to.capacity, to.contents]] | {
+        to.contents' = add[to.contents, moved]
+        from.contents' = subtract[from.contents, moved]
+    }
+    all b2: Bucket - (from + to) | b2.contents' = b2.contents
+}
+
+run {
+    initial
+    always {
+        (some b: Bucket | fill[b])
+        or
+        (some b: Bucket | empty[b])
+        or
+        (some from, to: Bucket | pour[from, to])
+    }
+    eventually {some b: Bucket | b.contents = 4} 
+} for 5 Int, -- bitwidth
+  exactly 3 Bucket -- no other buckets in the world

forge/examples/basic/gameOfLife 2.frg

@@ -0,0 +1,142 @@
+#lang forge
+
+/*
+    Conway's Game of Life in Forge
+    Hunt for still-lifes, oscillators, and gliders
+    Andrew Wagner + Tim Nelson
+
+    This is a finite-trace, discrete-event model; transitions represent 
+    steps of the automaton, and states define which cells are alive at that time.
+    We use Forge's "is linear" annotation (analogous to Alloy's util/ordering) for
+    **each run** to efficiently constrain the shape of the underlying trace skeleton.
+
+    The rules decide which cells survive/die/appear based on counting neighbors.
+    We echo that by using actual counting in Forge, which means we need to be able
+    to count up to 8 (bitwidth = 3 Int) minimum. With integers as indexes, this 
+    gives us a convenient 8x8 board. 
+
+    Finally, since the GoL is infinite, we need to approximate the board. We use 
+    the toroidal approximation that is used by some GoL engines. 
+*/
+
+option verbosity 0 -- turn off all console spam
+
+-- This previously activated Andrew's game-of-life format output code; a .rle file 
+-- would be produced that could be opened in GoL engines. (This was a kind of 
+-- "custom visualization" before we had good support for it!) 
+-- It is not currently supported.
+-- option demo life 
+
+sig State {
+    alive: set Int->Int,
+    next: lone State
+}
+
+-- useful to have a handle on the first element; think of this
+-- helper sig as analogous to a wrapper LinkedList class that 
+-- holds a reference to the first node in the list.
+one sig Trace {
+    first: one State
+}
+
+fun neighborhoods[alyv: Int->Int]: Int->Int->Int->Int {
+    { r: Int, c: Int, r2: Int, c2: Int |
+        let rows = (add[r, 1] + r + add[r, -1]) |
+            let cols = (add[c, 1] + c + add[c, -1]) |
+                (r2->c2) in (alyv & ((rows->cols) - (r->c))) }
+}
+
+-- Add "test" keyword before "expect" to run these validation tests
+expect nhood_tests {
+    nhoodAlive: { some alyv: Int->Int | let nhood = neighborhoods[alyv] | 
+        some r, c: Int | nhood[r][c] not in alyv } for 5 Int is unsat
+    nhoodBound: { some alyv: Int->Int | let nhood = neighborhoods[alyv] | 
+        some r, c: Int | #nhood[r][c] > 8 }        for 5 Int is unsat // 11408ms
+    nhoodSat:   { some alyv: Int->Int | let nhood = neighborhoods[alyv] | 
+        some r, c: Int | some nhood[r][c] }        for 5 Int is sat
+}
+
+pred gameStep[s1, s2: State] {
+    let nhood = neighborhoods[s1.alive] |
+        let birthing = { r: Int, c: Int | (r->c) not in s1.alive and #nhood[r][c] in 3 } |
+            let surviving = { r : Int, c: Int | (r->c) in s1.alive and #nhood[r][c] in (2 + 3) } |
+                s2.alive = birthing + surviving
+}
+
+-- almost the same everywhere
+pred findTrace {
+  one last: State | no last.next
+  no next.(Trace.first) -- enforce handle is correct
+  one first: State | no next.first
+  all b: State | b not in b.^next -- no cycles
+  all b: State | some b.next => { -- connected by moves
+    gameStep[b, b.next]
+  }
+}
+
+pred nontrivial {
+    some s: State {
+        some r, c: Int | r->c not in s.alive
+        some r, c: Int | r->c in s.alive
+    }
+}
+
+------------
+
+-- We could express this as an instance as well, if we were willing to 
+-- fix a specific trace length in `inst` format. But to keep things simple,
+-- we just write a predicate that disallows living cells outside the center 
+-- of the board.
+pred niceInitial[s: State] {
+    -- Can't say #s.alive bigger than 3 w/o messing up wraparound
+    no s.alive[-4] -- nothing alive on row -4 ...
+    no s.alive[-3] 
+    no s.alive[2]  
+    no s.alive[3]
+    -- Note parens are necessary when using dot-join like this:
+    no s.alive.(-4) -- Nothing alive on column -4 ... 
+    no s.alive.(-3)
+    no s.alive.(2)
+    no s.alive.(3)
+
+    s.alive in (-1 + -2 + 0 + 1)
+               -> 
+               (-1 + -2 + 0 + 1)
+}
+
+pred oscillator {
+    niceInitial[Trace.first] -- narrow window for readability
+
+    -- first state loops, but non-trivially
+    -- (relies on the predicate being run for only 3-state traces)
+    Trace.first.alive != Trace.first.next.alive    
+    Trace.first.alive = Trace.first.next.next.alive
+}
+
+pred glider {
+    some alive    
+    niceInitial[Trace.first] -- narrow window for readability
+
+    -- There's some transpose (possibly across toroidal bounds)
+    some future: State | { 
+        some next.future 
+        some xoffset, yoffset: Int | {
+            xoffset != 0 or yoffset != 0
+            all r, c: Int |
+                r->c in Trace.first.alive iff
+                (add[r, xoffset])->
+                (add[c, yoffset]) in future.alive
+        }
+    } 
+}
+
+---------------------------------------------------------------------
+
+-- Note the "next is linear" annotations; this efficiently encodes 
+-- well-formedness constraints on the shape of the trace.
+
+-- Find an oscillator (only 3 states are needed; see predicate)
+runOscillator : run { findTrace and oscillator } for 3 Int, 3 State for {next is linear}
+
+-- Find a period-4 glider (5 states = 4 transitions)
+runGlider : run { findTrace and glider } for 3 Int, 5 State for {next is linear}

forge/examples/basic/schoolPuzzle 2.frg

@@ -0,0 +1,48 @@
+#lang forge
+
+/*
+  Example puzzle model:
+
+  Alice supervises Bob
+  Bob supervises Charlie
+  Alice went to Brown
+  Charlie did not go to Brown
+  
+  Does a Brown graduate supervise a non-Brown graduate?
+*/
+
+sig School {}
+one sig Brown extends School {}
+one sig Harvale extends School {}
+
+sig Person {
+    supervises: lone Person,
+    school: one School
+    }
+one sig Alice extends Person {}
+one sig Bob extends Person {}
+one sig Charlie extends Person{}
+
+pred known {
+    supervises = Alice->Bob + Bob->Charlie
+    Alice->Brown in school
+    Charlie->Brown not in school
+}
+
+--known2 : run known for 3 Person, 2 School
+--known3 : run known for 3 Person, 3 School
+--------------------------------------------------------
+
+pred somebody {
+    some p: Person | some s: Person | {
+        p.school != Brown
+        s.school = Brown
+        p in s.supervises
+    }
+}
+pred nobody { not somebody }
+
+-- Reverse!
+--revpuzzle : run {known somebody} for exactly 3 Person, exactly 2 School
+-- Actual puzzle (expect unsat)
+--puzzle : run {known nobody} for exactly 3 Person, exactly 2 School

forge/examples/basic/traceSkeletonInst 2.frg

@@ -0,0 +1,20 @@
+#lang forge
+
+/*
+  Example of defining a trace skeleton using `inst` manually.
+*/
+
+option verbosity 10
+
+sig State { successor: set State }
+sig Initial extends State {}
+
+inst myExample {
+    State = `State0 + `State1 + `State2 + `State3
+    Initial = `State3
+    successor = `State3->`State0 + `State0->`State0 + `State0->`State3 + 
+                `State1->`State2 + `State2->`State1 + `State1->`State1 + 
+                `State2->`State2
+}
+
+run {} for myExample