diff --git a/forge/examples/README.md b/forge/examples/README.md index d033aa8f..f9e44e7f 100644 --- a/forge/examples/README.md +++ b/forge/examples/README.md @@ -1,9 +1,26 @@ -# Examples of Modeling in Forge (2023) +# Examples of Modeling in Forge -This folder contains a number of curated examples in Forge. +This folder contains a number of curated examples in Forge, from various sources. Some were previously in the [public examples repository](https://github.com/csci1710/public-examples/) for CSCI 1710 at Brown, or in the [lecture notes](https://csci1710.github.io/book/) for the class. As of June 2024, this directory is now the canonical home for them all. *Prior sources will not be kept up to date.* -For additional examples, see: -* The [CSCI 1710 public examples repo](https://github.com/csci1710/public-examples/) -* The [Forge documentation](https://csci1710.github.io/forge-documentation/) -* The [CSCI 1710 lecture notes](https://csci1710.github.io/2023/) +While many of these examples are commented more heavily, the [Forge documentation](https://csci1710.github.io/forge-documentation/) may still be useful. +## Directory Structure + +* `examples/basic/` contains a set of basic examples of Forge use, taken from various demos. +* `examples/tic_tac_toe` contains a model of the game tic-tac-toe, along with a custom visualizer. +* `examples/oopsla24` contains the models used in the Forge paper to appear at OOPSLA 2024. +* `examples/musical_scales` contains a basic model of diatonic scales, with a "visualizer" that also plays the scales generated. +* `examples/unsat` contains a set of toy examples demonstrating how unsat cores work in Forge, as of Spring 2024. +* `examples/sudoku_opt_viz` contains a sequence of models to solve Sudoku, demonstrating some optimization tricks and a visualizer for game boards. +* `examples/lights_puzzle` contains a model of a common puzzle involving rings or chains of lights that must be lit via switches that alter multiple lights' state at once. +* `examples/bsearch_array` contains a model of binary search on a sorted array, along with verification of some invariants. +* `examples/bst` contains a series of models of binary search trees. + - `bst_1.frg` and `bst_2.frg` are in Relational Forge, and focus on structural invariants for trees and the BST invariant (vs. an incorrect version). `bst_3.frg` and `bst_4.frg` are in Temproal Forge and model a recursive descent on an arbitrary tree following the correct vs. incorrect invariant. Both the Relational and Temporal Forge versions have visualization scripts. + +For a more advanced example, see: + +* `examples/prim`, which contains a model of Prim's MST algorithm, with notes on verification. + +## A Note on Visualization + +Some of these examples use "old style" visualizer scripts, i.e., from 2022 and 2023. These should still work as normal, but please report any issues! diff --git a/forge/examples/booleanLogic.frg b/forge/examples/basic/booleanLogic.frg similarity index 100% rename from forge/examples/booleanLogic.frg rename to forge/examples/basic/booleanLogic.frg diff --git a/forge/examples/basic/buckets.frg b/forge/examples/basic/buckets.frg new file mode 100644 index 00000000..e8aeeff1 --- /dev/null +++ b/forge/examples/basic/buckets.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 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 diff --git a/forge/examples/gameOfLife.frg b/forge/examples/basic/gameOfLife.frg similarity index 100% rename from forge/examples/gameOfLife.frg rename to forge/examples/basic/gameOfLife.frg diff --git a/forge/examples/schoolPuzzle.frg b/forge/examples/basic/schoolPuzzle.frg similarity index 100% rename from forge/examples/schoolPuzzle.frg rename to forge/examples/basic/schoolPuzzle.frg diff --git a/forge/examples/traceSkeletonInst.frg b/forge/examples/basic/traceSkeletonInst.frg similarity index 100% rename from forge/examples/traceSkeletonInst.frg rename to forge/examples/basic/traceSkeletonInst.frg diff --git a/forge/examples/bsearch_array/binarysearch.frg b/forge/examples/bsearch_array/binarysearch.frg new file mode 100644 index 00000000..9008ba5c --- /dev/null +++ b/forge/examples/bsearch_array/binarysearch.frg @@ -0,0 +1,262 @@ +#lang forge/bsl + +/* + Rough model of binary search on an array of integers. + + Recall: binary search (on an array) searches the array as if it embedded a tree; each step narrows + the range-to-be-searched by half. + + Tim Feb 2023/2024 +*/ + +----------------------------------------------------------- +-- Data definitions: integer arrays +----------------------------------------------------------- + +// Model an array of integers as a partial function from ints to ints. +// For ease of modeling, we'll also explicitly represent the length of the array. +// Also for ease of modeling, we'll just allow one array to exist in each instance. +one sig IntArray { + elements: pfunc Int -> Int, + lastIndex: one Int +} + +-- An IntArray is well-formed if this predicate returns true for it. +pred validArray[arr: IntArray] { + -- no elements before index 0 + all i: Int | i < 0 implies no arr.elements[i] + + -- if there's an element, either i=0 or there's something at i=1 + -- also the array is sorted: + all i: Int | some arr.elements[i] implies { + i = 0 or some arr.elements[subtract[i, 1]] + arr.elements[i] >= arr.elements[subtract[i, 1]] + } + -- lastIndex reflects actual size of array + all i: Int | (no arr.elements[i] and some arr.elements[subtract[i, 1]]) implies { + arr.lastIndex = subtract[i, 1] + } + {all i: Int | no arr.elements[i]} implies + {arr.lastIndex = -1} + +} + +-- Helper function to get the first index of the array; will be either 0 or -1. +fun firstIndex[arr: IntArray]: one Int { + arr.lastIndex = -1 => -1 else 0 +} + +----------------------------------------------------------- +-- Data definitions: Binary search +----------------------------------------------------------- + +-- Model the current state of a binary-search run on the array: the area to be searched +-- is everything from index [low] to index [high], inclusive of both. The [target] is +-- the value being sought, and [arr] is the entire array being searched. +sig SearchState { + arr: one IntArray, -- never changes + low: one Int, -- changes as the search runs + high: one Int, -- changes as the search runs + target: one Int -- never changes +} + +----------------------------------------------------------- + +-- What is an initial state of the search? There are many, depending on the actual +-- array and the actual target. But it should be a valid array, and it should start +-- with the obligation to search the entire array. +pred init[s: SearchState] { + validArray[s.arr] + s.low = firstIndex[s.arr] + s.high = s.arr.lastIndex + -- Note: we have written no constraints on the target; it may be any value +} + +----------------------------------------------------------- +-- Transition predicates +-- - stepNarrow (binary search narrows the [low, high] interval) +-- - stepSucceed (binary search finishes, finding the target) +-- - stepFailed (binary search finishes, not finding the target) +----------------------------------------------------------- + +pred stepNarrow[pre: SearchState, post: SearchState] { + -- mid = (low+high)/2 (rounded down) + let mid = divide[add[pre.low, pre.high], 2] | { + -- GUARD: must continue searching, this isn't the target + pre.arr.elements[mid] != pre.target + -- ACTION: narrow left or right + (pre.arr.elements[mid] < pre.target) + => { + -- need to go higher + post.low = add[mid, 1] + post.high = pre.high + } + else { + -- need to go lower + post.low = pre.low + post.high = subtract[mid, 1] + } + -- FRAME: the array and the target never change + post.arr = pre.arr + post.target = pre.target + } +} + +----------------------------------------------------------- + +-- Termination condition for the search: if low > high, we should stop. +-- "Do nothing" now; the search is over. +pred stepFailed[pre: SearchState, post: SearchState] { + -- GUARD: low and high have crossed + pre.low > pre.high + -- ACTION: no change in any field + post.arr = pre.arr + post.target = pre.target + post.low = pre.low + post.high = pre.high +} +-- Termination condition for the search: if we found the element, stop. +-- "Do nothing" now; the search is over. +pred stepSucceed[pre: SearchState, post: SearchState] { + -- GUARD: mid element = target + let mid = divide[add[pre.low, pre.high], 2] | + pre.arr.elements[mid] = pre.target + -- ACTION: no change in any field + post.arr = pre.arr + post.target = pre.target + post.low = pre.low + post.high = pre.high +} + +----------------------------------------------------------- + +-- Make it easier to reason about the system with an overall +-- "take a step" predicate. +pred anyTransition[pre: SearchState, post: SearchState] { + stepNarrow[pre, post] or + stepFailed[pre, post] or + stepSucceed[pre, post] +} + +-- We will discover that binary search breaks when the array is too big. What "too big" is +-- depends on the bitwidth Forge is using. E.g., the default of 4 bits means Forge can represent +-- the interval [-8, 7]. If low=3 and high=5, then (low+high) = (3+5) = 8, which is too big, so +-- it wraps around to -8. +-- This behavior lets us find a _real problem_. Binary search (not so) famously breaks if the +-- array is too long. See: https://ai.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html) +pred safeArraySize[arr: IntArray] { + -- A bit conservative, but it works for the model + arr.lastIndex < divide[max[Int], 2] + -- Let's also assume the array is non-empty + arr.lastIndex >= 0 +} + +--------------------------------------------------------------------------------------------- +-- Some "is satisfiable" tests. These test for consistency, possibility, non-vacuity. +-- If we don't include tests like this, our verification will be worthless. To see an +-- extreme example of why, consider: "A implies B" is always true if "A" is unsatisfiable, +-- regardless of what B is. +--------------------------------------------------------------------------------------------- + +test expect { + -- Check that it's possible to narrow on the first transition (this is the common case) + narrowFirstPossible: { + some s1,s2: SearchState | { + init[s1] + safeArraySize[s1.arr] + stepNarrow[s1, s2] + } + } for exactly 1 IntArray, exactly 2 SearchState + is sat + + -- Check that we can succeed immediately (likely because the target is in the middle exactly) + doneSucceedFirstPossible: { + some s1,s2: SearchState | { + init[s1] + safeArraySize[s1.arr] + stepSucceed[s1, s2] + } + } for exactly 1 IntArray, exactly 2 SearchState + is sat +} + +--------------------------------------------------------------------------------------------- +-- Some assertions: these check that counterexamples don't exist, meaning they _cannot_ check +-- for consistency as the tests above do. +--------------------------------------------------------------------------------------------- + +pred unsafeOrNotInit[s: SearchState] { + not init[s] or not safeArraySize[s.arr] +} +-- Check: Since we start with high >= low, the failure condition can't be reached in first state +-- unless the array is unsafe. +assert all s1, s2: SearchState | stepFailed[s1, s2] is sufficient for unsafeOrNotInit[s1] + for exactly 1 IntArray, exactly 2 SearchState + +-- The central invariant of binary search: +-- If the target is present, it's located between low and high +pred bsearchInvariant[s: SearchState] { + + all i: Int | { + s.arr.elements[i] = s.target => { + -- This has the side effect of saying: if the target is there, we never see low>high + s.low <= i + s.high >= i + + -- This is an example of how we need to _enrich_ the invariant in order to verify the property. + -- Counter-intuitively, it's easier for Forge to prove something stronger! The strengthening + -- says: low and high must be "reasonable" at all times. + s.low >= firstIndex[s.arr] + s.low <= s.arr.lastIndex + s.high >= firstIndex[s.arr] + s.high <= s.arr.lastIndex + + -- Note: these _technically_ should apply if the item is missing, too. But we'd need to be + -- more careful, if we wanted to move these outside the implication, because a 1-element array + -- (low=0; high=1) would end up with low>high and depending on how we model that, high could + -- "unreasonably" become -1. (high := mid-1). So for brevity we put the enrichment here. + + } + } + + -- To avoid the "array is too large" problem with binary search. + safeArraySize[s.arr] + + -- validArray should be preserved as well + validArray[s.arr] +} + +---------------------------------------------------------------------------- +-- Inductively verify that binary search preserves the (enriched) invariant. +-- Step 1: Initiation: check that init states must satisfy the invariant. +-- Step 2: Consecution: legal transitions preserve the invariant. +---------------------------------------------------------------------------- + +-- Step 1 +pred safeSizeInit[s: SearchState] { init[s] and safeArraySize[s.arr] } +assert all s: SearchState | safeSizeInit[s] is sufficient for bsearchInvariant[s] + for exactly 1 IntArray, exactly 1 SearchState + +-- Step 2 +pred stepFromGoodState[s1, s2: SearchState] { + bsearchInvariant[s1] + anyTransition[s1,s2] +} +assert all s1, s2: SearchState | stepFromGoodState[s1,s2] is sufficient for bsearchInvariant[s2] + for exactly 1 IntArray, exactly 2 SearchState + +-- These pass (but only after we add the enrichment). +-- To see an example, uncomment the run below. + +option run_sterling "binarysearch.js" +run { + some disj s1,s2: SearchState | { + init[s1] + validArray[s1.arr] + safeArraySize[s1.arr] + anyTransition[s1, s2] + -- To make things interesting, let's see a transition where the target is present + some i: Int | s1.arr.elements[i] = s1.target + } +} for exactly 1 IntArray, exactly 2 SearchState + diff --git a/forge/examples/bsearch_array/binarysearch.js b/forge/examples/bsearch_array/binarysearch.js new file mode 100644 index 00000000..1038f8ff --- /dev/null +++ b/forge/examples/bsearch_array/binarysearch.js @@ -0,0 +1,77 @@ +/* + Script for Binary Search example + + ASSUMES: all sigs as written in binarysearch.frg +*/ + +//////////////////////////////////////////////////////////// + +/** Helper to extract the atom from a singleton + * Note: this does not convert to the atom's id(); may get wrapping [] */ +function atomOf(expr, row, col) { + if(!('empty' in expr) || !('tuples' in expr)) throw `atomOf: expected expression, got: ${expr}` + if(expr.length < row-1) throw `atomOf: number of rows insufficient: ${expr}` + if(!expr.empty()) { + if(expr.tuples()[row] === undefined) + throw `atomOf: got undefined for ${row}th tuple in ${expr.tuples()[row]}` + if(expr.tuples()[row].atoms()[col] === undefined) + throw `atomOf: got undefined for ${col}th column in ${row}th tuple of ${expr.tuples()[row]}` + return expr.tuples()[row].atoms()[col] + } + return 'none' +} +/** Helper that returns a filter-function that filters for a specific set of atom IDs */ +function atomIdIn(idArr) { + return atomObj => atomObj.id() in idArr +} + +//////////////////////////////////////////////////////////// + +// Should only be one array +const arrays = IntArray.tuples().map(ltup => atomOf(ltup, 0, 0)) +const arrayElements = (arrays[0]).join(elements).tuples() +const states = SearchState.tuples().map(ltup => atomOf(ltup, 0, 0)) +const targetElement = atomOf(SearchState.join(target), 0, 0) + +const arrayGridConfig = { + // Absolute location in parent (here, of the stage itself) + grid_location: { x:10, y:150}, + // How large is each cell? + cell_size: {x_size:80,y_size:50}, + // How many rows and columns? + grid_dimensions: { + // One row for each state + y_size:states.length, + // One column for every entry in the array (plus state label) + x_size:arrayElements.length + 1}} + +const arrayGrid = new Grid(arrayGridConfig) + +// Populate a row in the table for each state +states.forEach((stateVal, stateIdx) => { + // Populate label + arrayGrid.add({x: 0, y: stateIdx}, new TextBox({text: `${stateVal.id().replace('SearchState','S')}`})); + // Identify low/high + const lowAtom = atomOf(stateVal.join(low), 0, 0) + const highAtom = atomOf(stateVal.join(high), 0, 0) + // Populate array + arrayElements.forEach((eVal, eIdx) => { + const indexAtom = atomOf(eVal, 0, 0) + const valueAtom = atomOf(eVal, 0, 1) + const labels = `${lowAtom.id() == indexAtom ? 'L' : ''}${highAtom.id() == indexAtom ? 'H' : ''}` + arrayGrid.add({x: parseInt(indexAtom.id())+1, y: stateIdx}, + new TextBox({text: `${valueAtom} ${labels}`, color: valueAtom.id() == targetElement.id() ? 'red' : 'black'})) + }) +}) + +// Finally, render everything +const stage = new Stage() +stage.add(arrayGrid) +stage.render(svg) + + + + + + + diff --git a/forge/examples/bst/README.md b/forge/examples/bst/README.md new file mode 100644 index 00000000..fa0a49f5 --- /dev/null +++ b/forge/examples/bst/README.md @@ -0,0 +1,18 @@ +# Binary Search Trees + +## Files + +* `bst_1.frg`: a Relational Forge model of binary trees +* `bst_2.frg`: a Relational Forge model of binary search trees (BSTs), using two different invariants +* `bst_3.frg`: a Temporal Forge model of search-descent through a BST, trying both invariants +* `bst_4.frg`: a Temporal Forge model of search-descent through a BST, checking correctness +* `bst.js`: visualization script for the Relational Forge models +* `bst_temporal.js`: visualization script for the Temporal Forge model + +There are also 2 example visualization images: +* `v1_success.png`: shows a successful binary-search run; +* `v2_failure.png`: shows a failed binary_search run (caused by a bad invariant). + +## TODO + +* Would be nice to have an alternative visualization that spaced the values out properly on a number line. This would make it easier to see the invariant(s). \ No newline at end of file diff --git a/forge/examples/bst/bst.frg b/forge/examples/bst/bst.frg new file mode 100644 index 00000000..5f28480d --- /dev/null +++ b/forge/examples/bst/bst.frg @@ -0,0 +1,96 @@ +#lang forge +option run_sterling "bst.js" + +/* + Model of binary search trees + Tim, 2024 +*/ + +sig Node { + key: one Int, -- every node has some key + left: lone Node, -- every node has at most one left-child + right: lone Node -- every node has at most one right-child +} +fun descendantsOf[ancestor: Node]: set Node { + ancestor.^(left + right) -- nodes reachable via transitive closure +} +pred binary_tree { + -- no cycles (modified) + all n: Node | + n not in descendantsOf[n] + -- connected via finite chain of left, right, and inverses + all disj n1, n2: Node | n1 in n2.^(left + right + ~left + ~right) + -- left+right differ (unless both are empty) + all n: Node | some n.left => n.left != n.right + -- nodes have a unique parent (if any) + all n: Node | lone parent: Node | n in parent.(left+right) +} +--run {binary_tree} for 7 Node + + + +run {binary_tree} for exactly 10 Node + +-- original v allowed self-loops in the root! + +/* +option solver MiniSat -- use native solver (menu item in Alloy) + + +pred req_unique_root { + {binary_tree and some Node} implies + {one root: Node | + all other: Node-root | other in descendantsOf[root]}} +test expect { + {not req_unique_root} for 7 Node is unsat +} +*/ +------------- +/* +pred binary_search_tree { + binary_tree -- a binary tree, with an invariant + all n: Node | { + -- "Every node's descendents..." + all d: n.left.*(left+right) | d.key < n.key + all d: n.right.*(left+right) | d.key > n.key + } +} +pred binary_search_tree_alternate { + binary_tree -- a binary tree, with an invariant + all n: Node | { + -- "Every node's immediate children..." + some n.left implies n.left.key < n.key + some n.right implies n.right.key > n.key + } +} +-- examples of the difference between the two +bstdiff: run {not { binary_search_tree iff binary_search_tree_alternate}} for 5 Node + + +*/ + + +/* +-- height: one Int, -- defined below +pred heights { + all n: Node | { + n.height = add[max[n.left.height+n.right.height], 1] }} +pred balanced { + -- child subtree heights differ by at most one + all n: Node | let diff = minus[n.left.height, n.right.height] | { + diff <= 1 and diff >= -1}} +run example_balanced { + binary_search_tree heights balanced} for 7 Node expect 1 + +-- Validation: expect 3-node chain to not be balanced +assert req_three_node_chain_unbalanced { + {binary_tree + heights + some disj n1, n2, n3: Node | { + no n: Node | n not in (n1+n2+n3) + n2 = n1.left and n3 = n2.left + }} implies not balanced +} +check req_three_node_chain_unbalanced for 7 Node + +*/ diff --git a/forge/examples/bst/bst.js b/forge/examples/bst/bst.js new file mode 100644 index 00000000..fb39bafc --- /dev/null +++ b/forge/examples/bst/bst.js @@ -0,0 +1,57 @@ +/* + Script for bst.frg. Expectations: + - sig Node { left: lone Node, right: lone Node } + - binary_tree pred is satisfied (e.g., unique root exists) + - no empty trees +*/ + +const RADIUS = 16; +const LEAF_RADIUS = 2; + +function makeLeaf() { + return { + visualObject: new Circle({radius:LEAF_RADIUS, color: 'black', borderColor: 'black'}), + children: [] } +} + +function firstAtomOf(expr) { + if(!expr.empty()) + return expr.tuples()[0].atoms()[0].id() + return 'none' +} + +// Construct a nested JS object that describes the tree structure. +function buildNested(root) { + let obj = new Circle({radius: RADIUS, color: 'white', borderColor: 'black', + label: firstAtomOf(root.key)}); + let dataTree = { visualObject: obj, children: []} + dataTree.children[0] = root.left.empty() ? + makeLeaf() : buildNested(root.left) + dataTree.children[1] = root.right.empty() ? + makeLeaf() : buildNested(root.right) + return dataTree +} + +// Which node is the root of the tree? +function findRoot() { + const noParents = Node.atoms().filter(a => left.join(a).empty() && + right.join(a).empty()) + if(noParents.length != 1) + throw Error('Instance had more than one root node: '+noParents) + return noParents[0] +} + +// A Tree takes a nested JS object that describes the tree structure. +const tree = new Tree({ + root: buildNested(findRoot()), + height: 500, + width: 500, + coords: { x: 20, y: 50 } + }); + +const stage = new Stage() +stage.add(tree) +stage.render(svg) + + + diff --git a/forge/examples/bst/bst_1.frg b/forge/examples/bst/bst_1.frg new file mode 100644 index 00000000..9852f95e --- /dev/null +++ b/forge/examples/bst/bst_1.frg @@ -0,0 +1,38 @@ +#lang forge +option run_sterling "./bst.js" + +/* + Model of binary search trees + Tim, 2024 + + First version: binary trees (without the BST invariant) +*/ + +sig Node { + key: one Int, -- every node has some key + left: lone Node, -- every node has at most one left-child + right: lone Node -- every node has at most one right-child +} +fun descendantsOf[ancestor: Node]: set Node { + ancestor.^(left + right) -- nodes reachable via transitive closure +} +pred binary_tree { + -- no cycles + all n: Node | n not in descendantsOf[n] + -- connected via finite chain of left, right, and inverses + all disj n1, n2: Node | n1 in n2.^(left + right + ~left + ~right) + -- left+right differ (unless both are empty) + all n: Node | some n.left => n.left != n.right + -- nodes have a unique parent (if any) + all n: Node | lone parent: Node | n in parent.(left+right) +} + +-- View a tree or two +run {binary_tree} for exactly 8 Node + +-- Run a test: our predicate enforces a unique root exists (if any node exists) +pred req_unique_root { + no Node or { + one root: Node | + all other: Node-root | other in descendantsOf[root]}} +assert binary_tree is sufficient for req_unique_root for 5 Node \ No newline at end of file diff --git a/forge/examples/bst/bst_2.frg b/forge/examples/bst/bst_2.frg new file mode 100644 index 00000000..285773c6 --- /dev/null +++ b/forge/examples/bst/bst_2.frg @@ -0,0 +1,69 @@ +#lang forge +option run_sterling "bst.js" + +/* + Model of binary search trees + Tim, 2024 + + Second version: binary trees with the BST invariant + + Note assumption: this model doesn't take duplicate entries into account. +*/ + +sig Node { + key: one Int, -- every node has some key + left: lone Node, -- every node has at most one left-child + right: lone Node -- every node has at most one right-child +} +fun descendantsOf[ancestor: Node]: set Node { + ancestor.^(left + right) -- nodes reachable via transitive closure +} +pred binary_tree { + -- no cycles + all n: Node | n not in descendantsOf[n] + -- connected via finite chain of left, right, and inverses + all disj n1, n2: Node | n1 in n2.^(left + right + ~left + ~right) + -- left+right differ (unless both are empty) + all n: Node | some n.left => n.left != n.right + -- nodes have a unique parent (if any) + all n: Node | lone parent: Node | n in parent.(left+right) +} + +-- View a tree or two +-- run {binary_tree} for exactly 10 Node + +-- Run a test: our predicate enforces a unique root exists (if any node exists) +pred req_unique_root { + no Node or { + one root: Node | + all other: Node-root | other in descendantsOf[root]}} +assert binary_tree is sufficient for req_unique_root for 5 Node + +--------------------------------------------------------------------------------- + +-- We have two potential predicates that might represent the ordering invariant. +-- One is correct, and the other is a common misunderstanding. + +pred invariant_v1[n: Node] { + -- "Every node's left-descendants..." via reflexive transitive closure + all d: n.left.*(left+right) | d.key < n.key + -- "Every node's left-descendants..." via reflexive transitive closure + all d: n.right.*(left+right) | d.key > n.key +} +pred binary_search_tree_v1 { + binary_tree -- a binary tree, with an added invariant + all n: Node | invariant_v1[n] +} +pred invariant_v2[n: Node] { + -- "Every node's immediate children..." + some n.left implies n.left.key < n.key + some n.right implies n.right.key > n.key +} +pred binary_search_tree_v2 { + binary_tree -- a binary tree, with an added invariant + all n: Node | invariant_v2[n] +} + +-- Get examples of the difference between the two. +bstdiff: run {not { binary_search_tree_v1 iff binary_search_tree_v2}} for 5 Node +-- These definitely not the same. Let's explore the impact of the difference. diff --git a/forge/examples/bst/bst_3.frg b/forge/examples/bst/bst_3.frg new file mode 100644 index 00000000..46873237 --- /dev/null +++ b/forge/examples/bst/bst_3.frg @@ -0,0 +1,158 @@ +#lang forge/temporal +option run_sterling "bst_temporal.js" + +/* + Model of binary search trees + Tim, 2024 + + Third version: temporally modeling a search-descent into the tree + + Note assumption: this model doesn't take duplicate entries into account. +*/ + +sig Node { + key: one Int, -- every node has some key + left: lone Node, -- every node has at most one left-child + right: lone Node -- every node has at most one right-child +} +fun descendantsOf[ancestor: Node]: set Node { + ancestor.^(left + right) -- nodes reachable via transitive closure +} +pred binary_tree { + -- no cycles + all n: Node | n not in descendantsOf[n] + -- connected via finite chain of left, right, and inverses + all disj n1, n2: Node | n1 in n2.^(left + right + ~left + ~right) + -- left+right differ (unless both are empty) + all n: Node | some n.left => n.left != n.right + -- nodes have a unique parent (if any) + all n: Node | lone parent: Node | n in parent.(left+right) +} + +-- View a tree or two +-- run {binary_tree} for exactly 10 Node + +-- Run a test: our predicate enforces a unique root exists (if any node exists) +pred req_unique_root { + no Node or { + one root: Node | + all other: Node-root | other in descendantsOf[root]}} +assert binary_tree is sufficient for req_unique_root for 5 Node + +--------------------------------------------------------------------------------- + +-- We have two potential predicates that might represent the ordering invariant. +-- One is correct, and the other is a common misunderstanding. + +pred invariant_v1[n: Node] { + -- "Every node's left-descendants..." via reflexive transitive closure + all d: n.left.*(left+right) | d.key < n.key + -- "Every node's left-descendants..." via reflexive transitive closure + all d: n.right.*(left+right) | d.key > n.key +} +pred binary_search_tree_v1 { + binary_tree -- a binary tree, with an added invariant + all n: Node | invariant_v1[n] +} +pred invariant_v2[n: Node] { + -- "Every node's immediate children..." + some n.left implies n.left.key < n.key + some n.right implies n.right.key > n.key +} +pred binary_search_tree_v2 { + binary_tree -- a binary tree, with an added invariant + all n: Node | invariant_v2[n] +} + +-- Get examples of the difference between the two. +-- bstdiff: run {not { binary_search_tree_v1 iff binary_search_tree_v2}} for 5 Node +-- These definitely not the same. Let's explore the impact of the difference. + +---------------------------------------------------------------------------------- + +-- Since a BST descent doesn't need to backtrack, the state can be fairly simple. +one sig SearchState { + target: one Int, -- fixed: the target of the search + var current: lone Node -- variable: the node currently being visited +} + +-- Initial-state predicate for the search +pred init { + -- Start at the root of the tree. + -- This formulation relies on uniqueness of the root, enforced elsewhere + SearchState.current = {n: Node | all other: Node-n | other in n.^(left+right)} + -- No constraints on the target value +} + +-- Transition predicates: descend from the current node into one of its children. +pred descendLeft { + -- GUARD + SearchState.target < SearchState.current.key + some SearchState.current.left + -- ACTION + SearchState.current' = SearchState.current.left +} +pred descendRight { + -- GUARD + SearchState.target > SearchState.current.key + some SearchState.current.right + -- ACTION + SearchState.current' = SearchState.current.right +} +-- Transition predicate: found target or a leaf; either way the search is over. +pred stop { + -- GUARD + SearchState.target = SearchState.current.key or + (SearchState.target > SearchState.current.key and no SearchState.current.right) or + (SearchState.target < SearchState.current.key and no SearchState.current.left) + -- ACTION (frame: do nothing) + SearchState.current' = SearchState.current +} + +-- VALIDATION +test expect { + -- let's check that these 3 transitions are mutually-exclusive + r_l_together: {eventually {descendLeft and descendRight}} for 7 Node is unsat + l_stop_together: {eventually {descendLeft and stop}} for 7 Node is unsat + r_stop_together: {eventually {descendRight and stop}} for 7 Node is unsat + -- let's check that these 3 are all possible to execute + r_sat: {eventually descendRight} for 7 Node is sat + l_sat: {eventually descendLeft} for 7 Node is sat + stop_sat: {eventually stop} for 7 Node is sat +} + +pred searchTrace { + init + always {descendLeft or descendRight or stop} +} + +-- Let's look at traces of the search using each version of the invariant. +-- If you use the custom visualizer, *visited* nodes will have a red border, +-- and *target* node(s) will have a thick border. + +-- We'll make this a bit more interesting, and tell Forge: +-- + not to show us immediate success/failure traces; and +-- + to show us traces where the target is present in the tree +run { + some Node -- non-empty tree + binary_search_tree_v1 -- use first invariant version + searchTrace -- do a search descent + not stop -- don't *immediately* succeed + not next_state stop -- don't succeed in 1 descent, either + SearchState.target in Node.key -- the target is present +} for exactly 8 Node +-- And the same using version 2: +run { + some Node -- non-empty tree + binary_search_tree_v2 -- use second invariant version + searchTrace -- do a search descent + not stop -- don't *immediately* succeed + not next_state stop -- don't succeed in 1 descent, either + SearchState.target in Node.key -- the target is present +} for exactly 8 Node -- don't *immediately* succeed + +-- Use "Next Config" to move to a different tree example. +-- One of the two should eventually produce an instance witnessing the _failure_ of +-- binary search: a target in the tree that is never found. + +---------------------------------------------------------------------------------- \ No newline at end of file diff --git a/forge/examples/bst/bst_4.frg b/forge/examples/bst/bst_4.frg new file mode 100644 index 00000000..6ee71097 --- /dev/null +++ b/forge/examples/bst/bst_4.frg @@ -0,0 +1,171 @@ +#lang forge/temporal +option run_sterling "bst_temporal.js" + +/* + Model of binary search trees + Tim, 2024 + + Fourth and final version: temporally modeling a search-descent into the tree, + adding an assertion to check correctness. + + Note assumption: this model doesn't take duplicate entries into account. +*/ + +sig Node { + key: one Int, -- every node has some key + left: lone Node, -- every node has at most one left-child + right: lone Node -- every node has at most one right-child +} +fun descendantsOf[ancestor: Node]: set Node { + ancestor.^(left + right) -- nodes reachable via transitive closure +} +pred binary_tree { + -- no cycles + all n: Node | n not in descendantsOf[n] + -- connected via finite chain of left, right, and inverses + all disj n1, n2: Node | n1 in n2.^(left + right + ~left + ~right) + -- left+right differ (unless both are empty) + all n: Node | some n.left => n.left != n.right + -- nodes have a unique parent (if any) + all n: Node | lone parent: Node | n in parent.(left+right) +} + +-- View a tree or two +-- run {binary_tree} for exactly 10 Node + +-- Run a test: our predicate enforces a unique root exists (if any node exists) +pred req_unique_root { + no Node or { + one root: Node | + all other: Node-root | other in descendantsOf[root]}} +assert binary_tree is sufficient for req_unique_root for 5 Node + +--------------------------------------------------------------------------------- + +-- We have two potential predicates that might represent the ordering invariant. +-- One is correct, and the other is a common misunderstanding. + +pred invariant_v1[n: Node] { + -- "Every node's left-descendants..." via reflexive transitive closure + all d: n.left.*(left+right) | d.key < n.key + -- "Every node's left-descendants..." via reflexive transitive closure + all d: n.right.*(left+right) | d.key > n.key +} +pred binary_search_tree_v1 { + binary_tree -- a binary tree, with an added invariant + all n: Node | invariant_v1[n] +} +pred invariant_v2[n: Node] { + -- "Every node's immediate children..." + some n.left implies n.left.key < n.key + some n.right implies n.right.key > n.key +} +pred binary_search_tree_v2 { + binary_tree -- a binary tree, with an added invariant + all n: Node | invariant_v2[n] +} + +-- Get examples of the difference between the two. +--bstdiff: run {not { binary_search_tree_v1 iff binary_search_tree_v2}} for 5 Node +-- These definitely not the same. Let's explore the impact of the difference. + +---------------------------------------------------------------------------------- + +-- Since a BST descent doesn't need to backtrack, the state can be fairly simple. +one sig SearchState { + target: one Int, -- fixed: the target of the search + var current: lone Node -- variable: the node currently being visited +} + +-- Initial-state predicate for the search +pred init { + -- Start at the root of the tree. + -- This formulation relies on uniqueness of the root, enforced elsewhere + SearchState.current = {n: Node | all other: Node-n | other in n.^(left+right)} + -- No constraints on the target value +} + +-- Transition predicates: descend from the current node into one of its children. +pred descendLeft { + -- GUARD + SearchState.target < SearchState.current.key + some SearchState.current.left + -- ACTION + SearchState.current' = SearchState.current.left +} +pred descendRight { + -- GUARD + SearchState.target > SearchState.current.key + some SearchState.current.right + -- ACTION + SearchState.current' = SearchState.current.right +} +-- Transition predicate: found target or a leaf; either way the search is over. +pred stop { + -- GUARD + SearchState.target = SearchState.current.key or + (SearchState.target > SearchState.current.key and no SearchState.current.right) or + (SearchState.target < SearchState.current.key and no SearchState.current.left) + -- ACTION (frame: do nothing) + SearchState.current' = SearchState.current +} + +-- VALIDATION +test expect { + -- let's check that these 3 transitions are mutually-exclusive + r_l_together: {eventually {descendLeft and descendRight}} for 7 Node is unsat + l_stop_together: {eventually {descendLeft and stop}} for 7 Node is unsat + r_stop_together: {eventually {descendRight and stop}} for 7 Node is unsat + -- let's check that these 3 are all possible to execute + r_sat: {eventually descendRight} for 7 Node is sat + l_sat: {eventually descendLeft} for 7 Node is sat + stop_sat: {eventually stop} for 7 Node is sat +} + +pred searchTrace { + init + always {descendLeft or descendRight or stop} +} + +-- Let's look at traces of the search using each version of the invariant. +-- If you use the custom visualizer, *visited* nodes will have a red border, +-- and *target* node(s) will have a thick border. + +-- We'll make this a bit more interesting, and tell Forge: +-- + not to show us immediate success/failure traces; and +-- + to show us traces where the target is present in the tree +// run { +// some Node -- non-empty tree +// binary_search_tree_v1 -- use first invariant version +// searchTrace -- do a search descent +// not stop -- don't *immediately* succeed +// SearchState.target in Node.key -- the target is present +// } for exactly 8 Node +-- And the same using version 2: +// run { +// some Node -- non-empty tree +// binary_search_tree_v2 -- use second invariant version +// searchTrace -- do a search descent +// not stop -- don't *immediately* succeed +// SearchState.target in Node.key -- the target is present +// } for exactly 8 Node -- don't *immediately* succeed + +-- Use "Next Config" to move to a different tree example. +-- One of the two should eventually produce an instance witnessing the _failure_ of +-- binary search: a target in the tree that is never found. + +---------------------------------------------------------------------------------- +-- Finally, let's write an assertion that the first invariant does in fact work. +pred bs_correct { + all n: Node | { + n.key = SearchState.target => + eventually SearchState.current = n + } +} +pred lasso_v1 { + binary_search_tree_v1 -- use first invariant version + searchTrace -- generate any arbitrary search trace +} +assert lasso_v1 is sufficient for bs_correct for 5 Node + +-- Great! The check passed (at least, up to 5 nodes) \ No newline at end of file diff --git a/forge/examples/bst/bst_temporal.js b/forge/examples/bst/bst_temporal.js new file mode 100644 index 00000000..0aea9393 --- /dev/null +++ b/forge/examples/bst/bst_temporal.js @@ -0,0 +1,77 @@ +/* + Script for _temporal_ BST model. Expectations: + - sig Node { left: lone Node, right: lone Node } + - binary_tree pred is satisfied (e.g., unique root exists) + - no empty trees + + Note: because the underlying tree is not variable, we can re-use the relational-forge visualizer + for the tree and just augment it based on temporal data. + + A node with the target key will have a thick border. + A node that's visited will have a red border. +*/ + +const RADIUS = 16; +const LEAF_RADIUS = 2; + +function makeLeaf() { + return { + visualObject: new Circle({radius:LEAF_RADIUS, color: 'black', borderColor: 'black'}), + children: [] } +} + +function firstAtomOf(expr) { + if(!expr.empty()) + return expr.tuples()[0].atoms()[0].id() + return 'none' +} + +// Use temporal information about the descent +function wasVisited(n) { + return instances.some((i) => { + const localCurrent = SearchState.join(i.field('current')) + return firstAtomOf(n) == firstAtomOf(localCurrent) + }) +} +function isTargetKey(k) { + return firstAtomOf(SearchState.join(target)) == firstAtomOf(k) +} + +// Construct a nested JS object that describes the tree structure. +function buildNested(root) { + let obj = new Circle({radius: RADIUS, color: 'white', + borderColor: wasVisited(root) ? 'red' : 'black', + label: firstAtomOf(root.key), + borderWidth: isTargetKey(root.key) ? 4 : 1}); + let dataTree = { visualObject: obj, children: []} + dataTree.children[0] = root.left.empty() ? + makeLeaf() : buildNested(root.left) + dataTree.children[1] = root.right.empty() ? + makeLeaf() : buildNested(root.right) + return dataTree +} + +// Which node is the root of the tree? +function findRoot() { + const noParents = Node.atoms().filter(a => left.join(a).empty() && + right.join(a).empty()) + if(noParents.length != 1) + throw Error('Instance had more than one root node: '+noParents) + return noParents[0] +} + +// A Tree takes a nested JS object that describes the tree structure. +const tree = new Tree({ + root: buildNested(findRoot()), + height: 500, + width: 500, + coords: { x: 20, y: 100 } + }); + +const stage = new Stage() +stage.add(new TextBox({text: `Target: ${SearchState.join(target)}`, coords:{x:100, y:25}})) +stage.add(tree) +stage.render(svg) + + + diff --git a/forge/examples/bst/v1_success.png b/forge/examples/bst/v1_success.png new file mode 100644 index 00000000..cc450097 Binary files /dev/null and b/forge/examples/bst/v1_success.png differ diff --git a/forge/examples/bst/v2_failure.png b/forge/examples/bst/v2_failure.png new file mode 100644 index 00000000..ed1aa945 Binary files /dev/null and b/forge/examples/bst/v2_failure.png differ diff --git a/forge/examples/lights_puzzle/README.md b/forge/examples/lights_puzzle/README.md new file mode 100644 index 00000000..0da77d51 --- /dev/null +++ b/forge/examples/lights_puzzle/README.md @@ -0,0 +1,11 @@ +# Example: Solving light-switching puzzles + +Many video games contain some variation of a puzzle involving lights and switches. The goal is to get all of the lights lit (or unlit). Usually every light has a corresponding switch, and usually the switch reverses the current state of its light and its immediate neighbors. + +This is an attempt to model a puzzle like that, and includes an example visualization that uses Sterling's script view with temporal mode. See the `lights.js` file for visualizing using Sterling's `instances` variable. + +## What It Looks Like + +Here's a puzzle trace visualized using this script: + +![Trace visualization](example.png) diff --git a/forge/examples/lights_puzzle/example.png b/forge/examples/lights_puzzle/example.png new file mode 100644 index 00000000..e4663e81 Binary files /dev/null and b/forge/examples/lights_puzzle/example.png differ diff --git a/forge/examples/lights_puzzle/lights.js b/forge/examples/lights_puzzle/lights.js new file mode 100644 index 00000000..afd7caa2 --- /dev/null +++ b/forge/examples/lights_puzzle/lights.js @@ -0,0 +1,142 @@ +d3 = require('d3') +d3.selectAll("svg > *").remove(); + +STATE_HEIGHT = 100 + +// No guarantee that Light1 is immediately right +// of Light0, etc. So we need to build an ordering +// in advance, based on the "right" relation. +// Passing 'true' to atoms() says to include members of sub-signatures +numLights = instances[0].signature('Light').atoms(true).length + +idxToLight = {0: 0} // Light0 is first +lightToIdx = {0: 0} +// NOTE: this will break if >9 lights +for(i = 1; i<=numLights;i++) { + priorIdx = idxToLight[i-1]; + priorObject = instances[0].atom('Light'+priorIdx) + lightNum = priorObject.right.toString().slice(-1) + idxToLight[i] = lightNum + if(lightNum != 0) + lightToIdx[lightNum] = i +} +// Debugging +//console.log(lightToIdx) +//console.log(idxToLight) + +// select('svg') doesnt work here +// use select(svg) + +states = + d3.select(svg) + // is element for group in SVG + // D3 is based on these "sandwich" calls: + // there's no element yet, but there will be once the data is + // processed. Bind the data to those elements... + .selectAll('g') + // Here's the data to bind. The map just makes sure we have the array index + // Can use either old or new style anonymous functions + .data(instances.map(function(d,i) { + return {item: d, index: i} + })) + // Now, for every entry in that array... + .enter() + // Add a (finally) + .append('g') + // Give it a class, for ease of debugging and possible use in future visualizations + .classed('state', true) + // Give it an 'id' attribute that's the state index (used later for labeling) + .attr('id', d => d.index) + +// Now, for each state , add a to the group +states + .append('rect') + .attr('x', 10) + .attr('y', function(d) { + return 20 + STATE_HEIGHT * d.index + }) + .attr('width', 300) + .attr('height', STATE_HEIGHT) + .attr('stroke-width', 2) + .attr('stroke', 'black') + .attr('fill', 'transparent'); + +// Debugging code, used to confirm that the rects were being +// re-rendered every run, early in writing this script +// Leaving this in for illustrative purposes +// states +// .append("text") +// .style("fill", "black") +// .attr('y', function(d) { +// return 40 + 220 * d.index +// }) +// .attr('x', 50) +// // If we don't wrap in a function, will be same value for ALL states +// //.text(Math.random()); +// // Instead, provide a different random number for each state label +// .text(function(d) { +// return Math.random()}); + +// For each state , add a state index label +// Recall that 'd' here is a variable bound to a specific data element, +// in this case, a state +states + .append("text") + .style("fill", "black") + .attr('y', function(d) { + return 40 + STATE_HEIGHT * d.index + }) + .attr('x', 50) + .text(d => "State "+d.index); + + +// Now, within each state +lightGroups = + states + // ...as before, we want to bind the sub-data (light values WITHIN a state) + .selectAll('circle') + .data( function(d) { + inst = d.item + lit = inst.signature('Lit').tuples() + unlit = inst.signature('Unlit').tuples() + lights = lit.concat(unlit) + return lights.map( function (ld) { + return {item: ld, + index: lightToIdx[ld.toString().slice(-1)], + on: lit.includes(ld), + state: d.index} + }) + }) + // for each of them + .enter() + // Add a new sub-group + .append('g') + .classed('light', true) + +// Each light contains a circle... +lightGroups + .append('circle') + // useful for debugging in inspector + .attr('index', d => d.index) + .attr('state', d => d.state) + .attr('item', d => d.item) + .attr('r', 20) + .attr('cx', function(d) { + return 50 + d.index * 50 + }) + .attr('cy', function(d) { + return 70 + d.state * STATE_HEIGHT + }) + .attr('stroke', 'gray') + .attr('fill', function(ld){ + if(ld.on == true) return 'yellow'; + else return 'gray'; + }); + +// ...and an index label +lightGroups + .append('text') + .attr('y', d => 75 + d.state * STATE_HEIGHT) + .attr('x', d => 47 + d.index * 50) + .text(d=>d.index); + diff --git a/forge/examples/lights_puzzle/ring_of_lights.frg b/forge/examples/lights_puzzle/ring_of_lights.frg new file mode 100644 index 00000000..5fdb5d64 --- /dev/null +++ b/forge/examples/lights_puzzle/ring_of_lights.frg @@ -0,0 +1,72 @@ +#lang forge/temporal + +/* + When using the custom vis script, remember to click "Run" after + asking for a new trace or config! (the script doesn't re-run automatically) +*/ + +------------------------ +-- Puzzle infrastructure +------------------------ +abstract sig Light { + left: one Light, -- neighbor to left + right: one Light -- neighbor to right +} +var sig Lit, Unlit extends Light {} + +pred ring { + -- Connected + all x1, x2: Light | x2 in x1.^left and x2 in x1.^right + -- Opposites + left = ~right +} + +pred solved { + Lit = Light +} +pred init { + -- ONE specific init state, so we can sketch how to exclude loopback + -- to the very beginning + no Lit + Unlit = Light +} + +pred flip[switch: Light] { + -- Flip the switch for , which also flips the neighbors + Lit' = Lit - {x: switch+switch.left+switch.right | x in Lit} + + {x: switch+switch.left+switch.right | x not in Lit} +} + +// Look for a solution to the puzzle that involves at *least* 5 states (4 transitions) +option min_tracelength 5 +// We need more than 5 states to find a solution +option max_tracelength 10 + +option verbose 5 +run { + -- well-formedness constraints + ring + -- start in an initial state + init + + -- transition predicate: either flip a single light, or we're done + always { + -- Do nothing for a solved board. Otherwise, flip a switch + { + solved -- guard + Lit = Lit' -- action + } or { + not solved -- guard + one l: Light | flip[l] -- action + } + } + + -- find a trace that leads to a solved state + eventually solved + + -- If we wanted, we could exclude some unproductive behavior by adding, e.g.: + -- Loopback can't be to the beginning + --next_state { always { some Lit }} + +} +for exactly 5 Light diff --git a/forge/examples/musical_scales/scales.frg b/forge/examples/musical_scales/scales.frg new file mode 100644 index 00000000..246146b2 --- /dev/null +++ b/forge/examples/musical_scales/scales.frg @@ -0,0 +1,117 @@ +#lang forge/bsl + +/* + Synthesis of (western) musical scales + + Nim Telson Spring 2021 Logic for Systems + Updated to Froglet by Tim in Spring 2024 + + ASSUMPTIONS + ----------- + * standard western music-theory setting (unsure if we need to assume 12-TET?) + * The intervals are all that matter, not the tones + * intervals are always ascending, and are always of whole or half-step lengths + + WOULD LIKE TO + ------------- + * explore microtonal intervals + * optimization, but not really needed yet +*/ + +-- give more power to eliminate solutions that are symmetric to ones we've seen already +option sb 250 + +-- pre-load the script +option run_sterling "scales.js" + +-- An interval corresponds to a number of half-steps, and is followed by another Interval +abstract sig Interval { + hs: one Int, + next: one Interval +} +-- Intervals are partitioned into Whole and Half steps (provided the intervalSizes +-- predicate is being included)) +sig W extends Interval {} +sig H extends Interval {} + +-- Where does the scale begin, and with which interval? +one sig Start { + start: one Interval, + offset: one Int +} + +-- Well-formedness constraints +pred wellformed { + -- Interval sizes are as expected + all s: W | s.hs = 2 + all s: H | s.hs = 1 + -- Offsets are within one octave + Start.offset >= 0 + Start.offset < 12 + -- Intervals partition the octave + (sum s: Interval | s.hs) = 12 + all s1,s2: Interval | reachable[s1, s2, next] + all s: Interval | one next[s] +} + +-- Include this to force scales to be diatonic +pred diatonic { + -- expected number of whole and half-steps + -- (Not the most efficient way to phrase this...) + #W = 5 + #H = 2 + -- Half steps are separated + -- We'll be able to express this much more consisely in Relational Forge, + -- but for now, let's stick to Froglet. "No half step's successor or twice + -- successor is another half step" + all h1: H, h2: H | h1.next != h2 and h1.next.next != h2 + +} + +-------------------------------------------------------------------------------- +-- Synthesize some scales (in the logical sense of synthesis) +-------------------------------------------------------------------------------- + +-- Make sure that Forge can count to 12! (not factorial) +-- bitwidth=3: 8 ints [-4, 3] +-- bitwidth=4: 16 ints [-8, 7] +-- bitwidth=5: 32 ints [-16, 15] + + -- Note well: currently it is *REQUIRED* to give the numeric scope for _all_ these sigs. + -- Otherwise, the results may be inconsistent. Improvement forthcoming in Spring 2024. +run { + wellformed + diatonic +} for 7 Interval, 5 Int, 7 H, 7 W -- 7, 5, 2, 5 would be more efficient + +-------------------------------------------------------------------------------- +-- Testing +-------------------------------------------------------------------------------- + +-- This is a partial instance, used for optimization. Think of it like a re-usable +-- example. Here, it describes an ionian scale (but without saying what the offset +-- is, so expect there are 12 possible ways to match it) +inst ionian { + H = `H2 + `H6 + W = `W0 + `W1 + `W3 + `W4 + `W5 + Interval = `W0 + `W1 + `H2 + `W3 + `W4 + `W5 + `H6 + Start = `Start0 + start = `Start0->`W0 + next = `W0 -> `W1 + + `W1 -> `H2 + + `H2 -> `W3 + + `W3 -> `W4 + + `W4 -> `W5 + + `W5 -> `H6 + + `H6 -> `W0 +} + +test expect { + ionianGenerated: { + wellformed + diatonic + } for + -- 5 W, 2 H would be more efficient, but this is a *TEST*. Leave room for issues to arise. + 7 W, 7 H, + 7 Interval, 5 Int for ionian is sat +} \ No newline at end of file diff --git a/forge/examples/musical_scales/scales.js b/forge/examples/musical_scales/scales.js new file mode 100644 index 00000000..a94a688a --- /dev/null +++ b/forge/examples/musical_scales/scales.js @@ -0,0 +1,617 @@ +require('d3') +require('tone') + +// Written by Mia Santomauro with advice from Tim Nelson in 2021. +// Minor changes to match 2024 Forge by Tim in February, 2024. + +// NOTE WELL: the require lines MUST be the first lines in the script, since +// this is an "old-style" custom visualizer. It is not an actual JavaScript require, +// but a directive to Sterling, listing modules to load from the JsDelivr CDN. + +// clear the svg +d3.selectAll("svg > *").remove(); +// set up tone synth +const synth = new tone.Synth().toDestination(); +// used for rendering and as a base for offset +const lowestNote = "C4"; + +/* + ___ _ _____ _ ___ _ _ _ _ ___ _____ ___ ___ _ _ ___ + | \ /_\_ _/_\ | __| | | | \| |/ __|_ _|_ _/ _ \| \| / __| + | |) / _ \| |/ _ \ | _|| |_| | .` | (__ | | | | (_) | .` \__ \ + |___/_/ \_\_/_/ \_\ |_| \___/|_|\_|\___| |_| |___\___/|_|\_|___/ + +*/ + +/** + * a function to parse the note notation for the letter, accidental, and octave + * @param {string} note + * @return {string[]} [letter, accidental, octave] + */ +function unpackNote(note) { + if (note.length === 2) { + return [note[0], "", note[1]]; + } else if (note.length === 3) { + return [note[0], note[1], note[2]]; + } else { + console.log("unsupported note format found in unpackNote: " + note); + } +} + +/** + * a function to remove the octave notation from the given note + * @param {string} note + */ +function truncNote(note) { + const [letter, accidental, octave] = unpackNote(note) + return letter + accidental; +} + +/** + * a function to extract out the id from the Forge Interval sigs + * @param {Interval[]} intervals the given intervals + * @param {Number[]} simpleIntervals an empty array to populate + */ +function constructSimpleIntervals(intervals, simpleIntervals) { + let i; + for (i = 0; i < intervals.length; i++) { + simpleIntervals.push(parseInt(intervals[i].hs._id)); + } +} + +/** + * a function to put a given array of intervals in order + * @param {Interval[]} intervals the given intervals + * @param {Interval[]} orderedIntervals an empty array to populate + */ +function constructOrderedIntervals(intervals, orderedIntervals) { + const firstInterval = Start0.start; + let currInterval = firstInterval; + orderedIntervals.push(firstInterval); + + let i; + for (i = 0; i < intervals.length - 1; i++) { + currInterval = currInterval.next; + orderedIntervals.push(currInterval); + } +} + +/** + * a function to order and simplify a given array of Intervals + * @param {Interval[]} intervals the given intervals + * @param {Number[]} simpleOrderedIntervals an empty array to populate + */ +function constructSimpleOrderedIntervals(intervals, simpleOrderedIntervals) { + const orderedIntervals = []; + constructOrderedIntervals(intervals, orderedIntervals); + constructSimpleIntervals(orderedIntervals, simpleOrderedIntervals) +} + +/* + __ __ _ _ ___ ___ ___ ___ _ _ _ _ ___ _____ ___ ___ _ _ ___ + | \/ | | | / __|_ _/ __| | __| | | | \| |/ __|_ _|_ _/ _ \| \| / __| + | |\/| | |_| \__ \| | (__ | _|| |_| | .` | (__ | | | | (_) | .` \__ \ + |_| |_|\___/|___/___\___| |_| \___/|_|\_|\___| |_| |___\___/|_|\_|___/ + +*/ + +// index corresponds to number of sharps +const SHARP_KEYS = ["G", "D", "A", "E", "B", "F#", "C#"]; +// index corresponds to number of flats +const FLAT_KEYS = ["F", "Bb", "Eb", "Ab", "Db", "Gb"]; +// index is arbitrary +const VALID_KEYS = ["C"] + SHARP_KEYS + FLAT_KEYS; +// index corresponds to position of tonic of relative major key +const MODES = ["ionian", "locrian", "aeolian", "mixolydian", "lydian", "phrygian", "dorian"]; + +/** + * a function to get the next letter alphabetically after the given letter, + * wrapping around back to A after G + * @param {string} letter + */ +function nextLetter(letter) { + return (letter === "G") ? "A" : String.fromCharCode(letter.charCodeAt(0) + 1); +} + +/** + * a function to get the previous letter alphabetically before the given letter, + * wrapping around back to G after A + * @param {string} letter + */ +function previousLetter(letter) { + return (letter === "A") ? "G" : String.fromCharCode(letter.charCodeAt(0) - 1); +} + +/** + * a function to get the note a half-step up from the given note + * @param {string} note + */ +function halfStep(note) { + let [letter, accidental, octave] = unpackNote(note); + // no accidental + if (accidental === "") { + if (letter === "B") { + let newOctave = parseInt(octave) + 1; + return "C" + newOctave; + } else if (letter === "E") { + return "F" + octave; + } else { + return letter + "#" + octave; + } + // sharp + } else if (accidental === "#") { + if (letter === "B") { + octave = parseInt(octave) + 1; + return "C#" + octave; + } else if (letter === "E") { + return "F#" + octave; + } else { + return nextLetter(letter) + octave; + } + // flat + } else if (accidental === "b") { + return letter + octave; + } else { + console.log("unsupported note format found in halfStep: " + note); + } +} + +/** + * a function to get the note a whole step up from the given note + * @param {string} note + */ +function wholeStep(note) { + return halfStep(halfStep(note)) +} + +/** + * a function to determine if the given interval represents a half step + * @param {Number} interval either 1 (half step) or 2 (whole step) + */ +function isHalfStep(interval) { + return interval === 1; +} + +/** + * a function to, given a starting note and a sequence of intervals, construct a scale + * @param {Number[]} intervals + * @param {string} startNote + * @param {string[]} notes the array to populate with the resulting scale. + */ +function getNotesFromIntervals(intervals, startNote, notes) { + + notes.push(startNote); + + let currNote = startNote; + let i; + for (i = 0; i < intervals.length; i++) { + // if the interval is a half-step... + if (isHalfStep(intervals[i])) { + currNote = halfStep(currNote); + } else { // if the interval is a whole-step... + currNote = wholeStep(currNote); + } + notes.push(currNote); + } +} + +/** + * a function to, given a sequence of intervals, + * determine the index of the note which represents + * the corresponding major key + * @param {Number[]} intervals + */ +function getMajorKeyIndex(intervals) { + // first interval is half step + if (isHalfStep(intervals[0])) { + // either phrygian or locrian + if (isHalfStep(intervals[3])) { + return 1; //locrian + } else { + return 5; // phrygian + } + // first interval is whole step + } else { + // either dorian, aeolian, ionian, lydian, or mixolydian + if (isHalfStep(intervals[1])) { + // either dorian, or aeolian + if (isHalfStep(intervals[4])) { + return 2; // aeolian + } else { + return 6; // dorian + } + } else { + // either ionian, lydian, or mixolydian + if (isHalfStep(intervals[2])) { + // ionian or mixolydian + if (isHalfStep(intervals[6])) { + return 0; // ionian + } else { + return 3; // mixolydian + } + } else { + return 4; //lydian + } + } + } +} + +/** + * given a sequence of intervals, + * determines the index of the note which + * represents the corresponding minor key + * @param {Interval[]} intervals + */ +function getMinorKeyIndex(intervals) { + const maj = getMajorKeyIndex(intervals); + return (maj + 5) % 7; +} + +/** + * Computes the equivalent note of opposite accidental for a given note. + * For example, D# ~= Eb and B# ~= C + * @param {string} note + */ +function getNoteEquiv(note) { + const [letter, accidental, octave] = unpackNote(note); + if (accidental === "") { + // TODO: check if it's E/F/B/C ? + return note; + } else { + if (accidental === "#") { + if (letter === "E") { + return "F" + octave; + } else if (letter === "B") { + const newOctave = parseInt(octave) + 1; + return "C" + newOctave; + } else { + return nextLetter(letter) + "b" + octave; + } + } else if (accidental === "b") { + if (letter === "F") { + return "E" + octave; + } else if (letter === "C") { + const newOctave = parseInt(octave) - 1; + return "B" + newOctave; + } else { + return previousLetter(letter) + "#" + octave; + } + } + } +} + +/** + * given an arbitrary key, return an equivalent one that is one the circle of fifths + * @param {string} key + */ +function getValidKey(key) { + const truncatedKey = truncNote(key); + + if (VALID_KEYS.includes(truncatedKey)) { + return key; + } else { + // TODO: double check that note equiv is a valid key + return getNoteEquiv(key); + } +} + +/** + * a function to determine whether the given key uses sharps in its key signature + * @param {string} key + */ +function keyUsesSharps(key) { + const truncatedKey = truncNote(key); + return SHARP_KEYS.includes(truncatedKey); +} + +/** + * a function to determine whether the given key uses flats in its key signature + * @param {string} key + */ +function keyUsesFlats(key) { + const truncatedKey = truncNote(key); + return FLAT_KEYS.includes(truncatedKey); +} + +/** + * a function to, given some notes and a key, fit the notes to that key + * such that they use the proper accidentals + * @param {string} key + * @param {*} notesApprox + * @param {*} notes an empty array to populate + */ +function fitNotesToKey(key, notesApprox, notes) { + + // TODO: this logic could be different to ensure note letters are incremental + // but this idea may only work for church modes and SOME other scales + + let toReplace = []; + if (keyUsesSharps(key)) { + toReplace.push("b"); + } else if (keyUsesFlats(key)) { + toReplace.push("#") + } else { + toReplace.push("b"); + toReplace.push("#"); + } + + let i; + for (i = 0; i < notesApprox.length; i++) { + let currNote = notesApprox[i]; + if (currNote.length === 3) { + if (toReplace.includes(currNote[1])) { + currNote = getNoteEquiv(currNote); + } + } + notes.push(currNote); + } +} + +/** + * a function to determine if the given sequence of intervals represents a church mode + * @param {*} intervals + */ +function isChurchMode(intervals) { + + const firstHalfStep = intervals.indexOf(1); + + if (firstHalfStep < 0 || firstHalfStep > 3) { + return false; + } + + const restOfIntervals = intervals.slice(firstHalfStep + 1); + const secondHalfStep = restOfIntervals.indexOf(1); + + if (secondHalfStep < 0 || secondHalfStep > 3) { + return false; + } + + if (secondHalfStep === 2) { + return [1, 2, 3].includes(firstHalfStep); + } else if (secondHalfStep === 3) { + return [0, 1, 2].includes(firstHalfStep); + } else { + return false; + } +} + +/* + ___ ___ _ _ _ _ ___ ___ _ _ _ _ ___ _____ ___ ___ _ _ ___ + / __|/ _ \| | | | \| | \ | __| | | | \| |/ __|_ _|_ _/ _ \| \| / __| + \__ \ (_) | |_| | .` | |) | | _|| |_| | .` | (__ | | | | (_) | .` \__ \ + |___/\___/ \___/|_|\_|___/ |_| \___/|_|\_|\___| |_| |___\___/|_|\_|___/ + +*/ + +/** + * a function to play the given scale aloud + * @param {string[]} notes the notes to play (in order) + */ +function playScale(notes) { + console.log(`playScale: ${notes}`) + const now = tone.now() + let i; + for (i = 0; i < notes.length; i++) { + synth.triggerAttackRelease(notes[i], "8n", now + (i * .5)); + } +} + +/* + __ _____ ____ ___ _ _ _ _ ___ _____ ___ ___ _ _ ___ + \ \ / /_ _|_ / | __| | | | \| |/ __|_ _|_ _/ _ \| \| / __| + \ V / | | / / | _|| |_| | .` | (__ | | | | (_) | .` \__ \ + \_/ |___/___| |_| \___/|_|\_|\___| |_| |___\___/|_|\_|___/ + +*/ + +const bottom = 400; +const left = 100; +const w = 25; +const margin = 30; + +/** + * a function to render the staff + */ +function drawStaff() { + let i; + for (i = 0; i < 5; i++) { + let y = bottom - (i * w) - w; + d3.select(svg) + .append("line") + .attr("x1", left) + .attr("y1", y) + .attr("x2", left + 500) + .attr("y2", y) + .attr("stroke", "black") + } +} + +/** + * a function to compute y value for a given note + * @param {string} note + */ +function noteToY(note) { + + let offset = 0; + let letter; + let octave; + + if (note.length === 2) { + letter = note[0]; + octave = note[1]; + } else if (note.length === 3) { + letter = note[0]; + octave = note[2]; + } + + const lowestOctave = parseInt(lowestNote[1]); + offset += (7 * (octave - lowestOctave)); + + const letterCharCode = letter.charCodeAt(0); + const lowestCharCode = lowestNote.charCodeAt(0); + + if (letterCharCode > lowestCharCode) { + offset += letterCharCode - lowestCharCode; + } else if (letterCharCode < lowestCharCode) { + offset += 7 - (lowestCharCode - letterCharCode) + } + + return bottom - (w * (offset / 2)) + +} + +/** + * a function to render the notes on the staff + * @param {string[]} notes + */ +function drawNotes(notes) { + console.log(`drawNotes: ${notes}`) + + const x = (note, index) => { + return index * (w + margin) + left + 20; // todo replace 20 with width of treble clef + } + + const y = (note, index) => { + return noteToY(note); + } + + const accX = (note, index) => { + return x(note, index) - 36; + } + + const accY = (note, index) => { + return y(note, index) + 5; + } + + const acc = (note) => { + if (note.length === 3) { + const accidental = note[1]; + if (accidental === "#") { + return "#" + } else if (accidental === "b") { + return "♭" + } + } + return "" + } + + const circles = d3.select(svg) + .selectAll('ellipse') + .data(notes) + .join('ellipse') + .attr('rx', w / 2 + 5) + .attr('ry', w / 2) + .attr('cx', x) + .attr('cy', noteToY) + .style('stroke', 'black') + .style('fill', 'white'); + + const accidentals = d3.select(svg) + .selectAll('text') + .data(notes) + .join('text') + .attr('x', accX) + .attr('y', accY) + .style("font", "24px times") + .text(acc); +} + +/** + * a function to display information about the scale + * @param {*} notes + * @param {*} majIndex + * @param {*} majKey + * @param {*} churchMode + */ +function printResult(notes, majIndex, majKey, churchMode) { + + if (churchMode) { + d3.select(svg) + .append("text") + .style("fill", "black") + .attr("x", 50) + .attr("y", 50) + .text("This is " + truncNote(notes[0]) + " " + MODES[majIndex]); + + d3.select(svg) + .append("text") + .style("fill", "black") + .attr("x", 50) + .attr("y", 70) + .text("which is in the key of " + truncNote(majKey) + " Major"); + } else { + d3.select(svg) + .append("text") + .style("fill", "black") + .attr("x", 50) + .attr("y", 50) + .text("This is not a church mode"); + } +} + +/** + * a function to construct the whole visualization + * @param {*} notes + * @param {*} majIndex + * @param {*} majKey + * @param {*} churchMode + */ +function constructVisualization(notes, majIndex, majKey, churchMode) { + drawStaff(); + drawNotes(notes); + printResult(notes, majIndex, majKey, churchMode); +} + +/* + __ __ _ ___ _ _ ___ _ _ _ _ ___ _____ ___ ___ _ _ + | \/ | /_\ |_ _| \| | | __| | | | \| |/ __|_ _|_ _/ _ \| \| | + | |\/| |/ _ \ | || .` | | _|| |_| | .` | (__ | | | | (_) | .` | + |_| |_/_/ \_\___|_|\_| |_| \___/|_|\_|\___| |_| |___\___/|_|\_| + +*/ + +function go(startNote) { + console.log(`startNote: ${startNote}`) + + // constructing ordered array of intervals + const intervals = Interval.atoms(true); + const simpleOrderedIntervals = [] + constructSimpleOrderedIntervals(intervals, simpleOrderedIntervals); + + // determine if this is a church mode + const churchMode = isChurchMode(simpleOrderedIntervals); + + // constructing the notes array + const notesApprox = []; + getNotesFromIntervals(simpleOrderedIntervals, startNote, notesApprox); + + // finding the relative major key + const majIndex = getMajorKeyIndex(simpleOrderedIntervals); + const majKeyApprox = notesApprox[majIndex]; + const majKey = getValidKey(majKeyApprox); + + // reconstructing the notes array + const notes = []; + fitNotesToKey(majKey, notesApprox, notes); + + // playing the scale out loud + playScale(notes); + + // rendering the scale on the staff + constructVisualization(notes, majIndex, majKey, churchMode); + +} + +const off = Start0.offset._id; + +let i; +let startNote = lowestNote; +for (i = 0; i < off; i++) { + startNote = halfStep(startNote); +} + +console.log(`Starting. startNote=${startNote}`) +go(startNote); + + + diff --git a/forge/examples/oopsla24/README.md b/forge/examples/oopsla24/README.md new file mode 100644 index 00000000..d5212064 --- /dev/null +++ b/forge/examples/oopsla24/README.md @@ -0,0 +1,3 @@ +# Examples from OOPSLA 2024 + +This directory contains the models used in the OOPSLA 2024 Forge paper. diff --git a/forge/examples/paper/f2_ttt.frg b/forge/examples/oopsla24/f2_ttt.frg similarity index 100% rename from forge/examples/paper/f2_ttt.frg rename to forge/examples/oopsla24/f2_ttt.frg diff --git a/forge/examples/paper/f3_nodes.frg b/forge/examples/oopsla24/f3_nodes.frg similarity index 100% rename from forge/examples/paper/f3_nodes.frg rename to forge/examples/oopsla24/f3_nodes.frg diff --git a/forge/examples/paper/f4_counter.frg b/forge/examples/oopsla24/f4_counter.frg similarity index 100% rename from forge/examples/paper/f4_counter.frg rename to forge/examples/oopsla24/f4_counter.frg diff --git a/forge/examples/paper/f8_testing.frg b/forge/examples/oopsla24/f8_testing.frg similarity index 100% rename from forge/examples/paper/f8_testing.frg rename to forge/examples/oopsla24/f8_testing.frg diff --git a/forge/examples/paper/f9_core.rkt b/forge/examples/oopsla24/f9_core.rkt similarity index 100% rename from forge/examples/paper/f9_core.rkt rename to forge/examples/oopsla24/f9_core.rkt diff --git a/forge/examples/paper/goat_cabbage_wolf.frg b/forge/examples/oopsla24/goat_cabbage_wolf.frg similarity index 100% rename from forge/examples/paper/goat_cabbage_wolf.frg rename to forge/examples/oopsla24/goat_cabbage_wolf.frg diff --git a/forge/examples/paper/goat_cabbage_wolf.js b/forge/examples/oopsla24/goat_cabbage_wolf.js similarity index 100% rename from forge/examples/paper/goat_cabbage_wolf.js rename to forge/examples/oopsla24/goat_cabbage_wolf.js diff --git a/forge/examples/paper/lab1_start.frg b/forge/examples/oopsla24/lab1_start.frg similarity index 100% rename from forge/examples/paper/lab1_start.frg rename to forge/examples/oopsla24/lab1_start.frg diff --git a/forge/examples/paper/net1.vis.js b/forge/examples/oopsla24/net1.vis.js similarity index 100% rename from forge/examples/paper/net1.vis.js rename to forge/examples/oopsla24/net1.vis.js diff --git a/forge/examples/prim/prim.frg b/forge/examples/prim/prim.frg new file mode 100644 index 00000000..c3a5e14a --- /dev/null +++ b/forge/examples/prim/prim.frg @@ -0,0 +1,337 @@ +#lang forge/temporal + +-- Default of 5; this model uses 1 time index per state +option max_tracelength 7 + +/* +Prim's algorithm in Forge + Tim, 2021; revised to use Temporal Forge in 2024 + + For visualization, use Table View and open the "Time" side drawer to step + through the trace; you should see a new Node being added to Prim.pnodes every step. + + Note that this model will take around a minute to run. Some of the + (passing) tests are somewhat inefficient. + +*/ + +------------------------------------------------------------- +-- Always have a specific weighted directed graph in the background +------------------------------------------------------------- + +sig Node { + edges: set Node -> Int +} + +pred wellformedgraph { + -- no differently-valued edges between the same nodes + all n, m: Node | lone edges[n][m] + + -- no negative weights + all n, m: Node | some edges[n][m] implies edges[n][m] >= 0 + + -- This isn't strong enough (it says: symmetric, **without** regard to weights): + -- edges.Int = ~(edges.Int) + -- This is strong enough (symmetric, with same weights required): + all n, m: Node | edges[n][m] = edges[m][n] + + -- no self-loops + no (iden & edges.Int) + + -- connected (or else it cannot be spanned) + all disj n, m: Node | n in m.^(edges.Int) +} + +-- Demo checking that the weight-aware symmetry constraint subsumes the other. +pred test_old { edges.Int = ~(edges.Int) } +pred test_new { all n, m: Node | edges[n][m] = edges[m][n] } +assert test_new is sufficient for test_old for 5 Node, 5 Int + +------------------------------------------------------------- +-- Prim's algorithm +------------------------------------------------------------- + +one sig Prim { + var pnodes: set Node, + var ptree: set Node->Node +} + +pred prim_init { + one Prim.pnodes -- one arbitrary node picked to start + no Prim.ptree -- no spanning tree edges yet +} + +-- Intermediate steps represented as helper predicates + +-- The set of possible nodes to expand the tree to next, along with costs +fun candidatesWithWeights: set Node -> Int { + ((Node-Prim.pnodes) -> Int) & Prim.pnodes.edges +} +-- The cheapest cost among all candidates +fun minCandidateWeight: set Int { + min[candidatesWithWeights[Node]] +} +-- The candidates who share that cheapest cost +-- (Note how you can use a helper function as a relation to join on!) +fun minWeightCandidates: set Node { + candidatesWithWeights.minCandidateWeight +} + +-- A little code duplication here, but it enables a richer validation below +pred prim_step_enabled[m, n: Node] { + m in Prim.pnodes -- source node is in the set + n in minWeightCandidates -- destination node is a minimal hop away + -- perhaps there's a more efficient way to do this line? + m->n->minCandidateWeight in edges -- there's an actual edge at this weight +} +pred prim_step[m, n: Node] { + -- GUARD + prim_step_enabled[m, n] + -- ACTION/FRAME for pnodes + Prim.pnodes' = Prim.pnodes + n + -- ACTION/FRAME for ptree (remember to add both symmetric edges!) + Prim.ptree' = Prim.ptree + (m -> n) + (n -> m) +} + +pred prim_doNothing { + -- GUARD + -- we cannot make progress using a Prim step -- DO NOT CONFUSE this with prim_step + all m_no, n_no: Node | not prim_step_enabled[m_no, n_no] + -- ACTION + Prim.pnodes' = Prim.pnodes + Prim.ptree' = Prim.ptree +} + + +----------------------------------------------- +-- Run! +----------------------------------------------- + +pred prim_trace { + wellformedgraph -- require a well-formed graph + prim_init -- start in an initial state + + -- always step forward using these transitions + always { + some m, n: Node | { prim_step[m, n] } + or + prim_doNothing + } +} + +------------------------------------------------------------- +-- View a run! +------------------------------------------------------------- + +--run prim_trace for exactly 5 Node, 5 Int + +------------------------------------------------------------- +-- Model Validation +------------------------------------------------------------- + +-- "Optional" predicates focusing on wellformedgraph, since our criterion for +-- finishing Prim's is that all the nodes are in the spanning tree. We want to +-- check that certain shapes are possible *AND* that Prim's can run on those shapes. +-- (The below combines these checks, since prim_trace includes wellformedgraph) + +-- Find a graph where all the edges are different lengths. +-- A broken version of this might be: +pred difflengthedges_broken { + all disj n1, n2: Node | all disj m1, m2: Node | { + (n1->m1 in edges.Int implies n1.edges[m1] != n2.edges[m2]) + } +} +-- Note how this breaks. Consider what happens if n1=m2 and m1=n2. + +-- Instead, here are two alternative fixes (of many): +pred difflengthedges { + all disj n1, n2: Node | all disj m1, m2: Node | { + (n1 != m2) implies + (n1->m1 in edges.Int implies n1.edges[m1] != n2.edges[m2]) + } +} +pred difflengthedges_2 { + all disj n1, n2: Node | all disj m1, m2: Node | { + #(n1 + m1 + n2 + m2) >= 3 implies + (n1->m1 in edges.Int implies n1.edges[m1] != n2.edges[m2]) + } +} +// Are 2 of these options equivalent? If yes, our confidence increases: +test expect { + {wellformedgraph implies {difflengthedges iff difflengthedges_2}} + for 5 Node is theorem +} + +-- Find a graph where all possible edges are present (at some weight) +pred complete_graph { + all disj n1, n2: Node | { + n1->n2 in edges.Int + } +} + +-- Run most of these on arbitrary 5-node graphs to force Forge to try more realistic cases. +test expect { + localize_a: {wellformedgraph and difflengthedges} + for exactly 5 Node, 5 Int is sat + + -- Make sure we can generate and run Prim's on graphs with different/same weights + prims_difflengths_5: {prim_trace and difflengthedges} + for exactly 5 Node, 5 Int is sat + prims_samelengths_5: {prim_trace and not difflengthedges} + for exactly 5 Node, 5 Int is sat + + -- Make sure we can generate and run Prim's on graphs of 1 and 2 nodes + -- (*Don't* expect 0-node graphs to work.) + prims_single_node: {prim_trace} + for exactly 1 Node, 5 Int is sat + prims_double_node: {prim_trace} + for exactly 2 Node, 5 Int is sat + + -- Make sure we can generate and run Prim's on complete/incomplete graphs + prims_complete_graph_5: {prim_trace and complete_graph} + for exactly 5 Node, 5 Int is sat + prims_non_complete_graph_5: {prim_trace and not complete_graph} + for exactly 5 Node, 5 Int is sat +} + +-- These are great, but... +-- We'd really love to check that Prim's can actually run on _every_ possible +-- non-empty graph. The problem is that Temporal Forge only finds lasso traces, +-- so "can actually run" must fit into a lasso trace. This is why doNothing's +-- guard is just "prim_step isn't enabled"; we want to allow even buggy lasso traces! + +test expect { + doNothing_not_used_buggily: { + -- Can we find a Prim trace where doNothing is used before the full tree is explored? + prim_trace + eventually {prim_doNothing and Prim.pnodes != Node} + } for 5 Node, 5 Int + -- Hopefully not! + is unsat +} + + + +------------------------------------------------------------- +-- Requirements +------------------------------------------------------------- + +-- (1) The spanning tree generated actually spans the graph, and +-- uses only valid edges +pred current_is_spanning { + -- Spans + all disj n1, n2: Node | n1 in n2.^(Prim.ptree) + -- Valid edges only + Prim.ptree in edges.Int +} +-- (2) The spanning tree generated is a tree +pred current_is_tree { + -- This is subtle to express for _undirected_ trees, since Forge represents them + -- as symmetric directed trees. We'll say "whenever two nodes are directly + -- connected, removing that connection removes connectivity between them" + all disj n1, n2: Node | n2 in n1.(Prim.ptree) implies { + n2 not in n1.^(Prim.ptree - (n1->n2 + n2->n1)) + } + -- Note that the symmetry is vital for this predicate to work. Otherwise, + -- consider N0 -> N1 -> N2 -> N0. +} +-- Note: make sure not to separate these into different time indexes: +-- "eventually current_is_spanning and eventually current_is_tree" +-- would allow starting as a tree but ending as a DAG! +pred req_eventually_is_spanning_tree { + eventually {current_is_spanning and current_is_tree } +} +assert prim_trace is sufficient for req_eventually_is_spanning_tree + for 5 Node, 5 Int + +------------------------------------------------------------------------------- + +-- (3) the spanning tree generated is minimal + +-- Minimality is much harder to express for the moment. The original model +-- this was taken from ran Kruskal's algorithm too, and compared the total +-- weight of the results: a variation of Property-Based Testing! + +-- ...but let's try to express minimality, anyway. +-- First, we need to pull the separate criteria into a predicate we can +-- check _other_ trees on. We'll copy from above, with minor edits: +pred isSpanningTree[t: set Node -> Node] { + -- is spanning: + all disj n1, n2: Node | n1 in n2.^t + -- is tree: + all disj n1, n2: Node | n2 in n1.t implies { + n2 not in n1.^(t - (n1->n2 + n2->n1)) + } + -- Since "t" is an arbitrary relation, and this definition of "tree" is for + -- the symmetric encoding of undirected trees, we need to require symmetry: + t = ~t + -- valid edges: + t in edges.Int +} +-- and we need to measure the weight of a given edge set: +fun totalWeight[eset: set Node -> Node]: one Int { + sum n1: Node | sum n2: Node | { + n1->n2 in eset => edges[n1][n2] + else 0 + } +} + +-- We might want to write a predicate like this, but it involves higher-order +-- universal quantification, and anyway Forge will reject this Alloy-style syntax: +/* +pred current_is_minimal_st { + -- Current state of Prim's is a spanning tree + isSpanningTree[Prim.ptree] + -- For all _other_ trees... (FORGE WILL NOT SUPPORT THIS SYNTAX!) + all t2: set Node -> Node | { + isSpanningTree[t2] implies totalWeight[t2] <= totalWeight[Prim.ptree] + } +} +*/ + +-- But verification is different. What happens if we try to flip the scenario, and +-- search for a counterexample? Forge, like Alloy, will handle higher-order existentials, +-- although we need to create a helper relation ourselves, rather than using Alloy-style syntax. + +-- Find a counterexample, i.e., a better spanning tree: +one sig Helper { + otherTree: set Node -> Node +} +pred counter_example_to_req_prim_is_minimal { + -- Finish running Prim's + prim_trace + -- But we also have some other tree that is better. + eventually { + -- Setup to avoid overflow, need to count much higher than edge weights can be + totalWeight[Helper.otherTree] > 0 + totalWeight[Prim.ptree] > 0 + all n1, n2: Node | n1->n2 in edges.Int implies edges[n1][n2] <= 2 + + -- Prim's is done at this point + isSpanningTree[Prim.ptree] + -- Other relation is a tree, spans, and is lower cost + isSpanningTree[Helper.otherTree] + totalWeight[Helper.otherTree] < totalWeight[Prim.ptree] + } +} +-- This takes longer to run than I am willing to wait. So we can express the goal, +-- but it is not compiled/solved efficiently. Some of the problem is symmetry, but also +-- the handling of integers for counting... +// test expect { +// no_ce: {counter_example_to_req_prim_is_minimal} for 5 Node, 5 Int is unsat +// } +-- Fortunately, we can recast this using an optimizer instance to limit edge +-- weights, rather than a constraint. Let's try it: +test expect { + no_ce_optimized: {counter_example_to_req_prim_is_minimal} + for 5 Node, 5 Int + for { + Node = `Node0 + `Node1 + `Node2 + `Node3 + `Node4 + -- Allow only 0, 1, and 2 as edge weights + edges in Node -> Node -> (0+1+2) + } + is unsat +} +-- With the optimizer instance, the test passes in about 2.5 minutes at max +-- trace length 7. + diff --git a/forge/examples/sudoku_opt_viz/README.md b/forge/examples/sudoku_opt_viz/README.md new file mode 100644 index 00000000..56a2f9cf --- /dev/null +++ b/forge/examples/sudoku_opt_viz/README.md @@ -0,0 +1,15 @@ +# Sudoku Solver / Synthesizer Example + +In this example, I try to optimize a sudoku model. I pass through multiple versions: +* sudoku_basic.frg +* sudoku_with_inst.frg +* sudoku_with_inst2.frg +* sudoku_unrolled.frg +* sudoku_rethink.frg + +Most files contain the first thing I tried: just generating a pair of unsolved/solved boards, with the unsolved board has 7 squares populated. The first and last file contain a run command to solve a hard sudoku puzzle. + +The repo also contains an example of a (rough) visualization: +* sudoku.js + +Note the visualization is meant for the two-board model, not the single-board model! It should illustrate how to get at fields, draw lines, print relations, etc. diff --git a/forge/examples/sudoku_opt_viz/sudoku.js b/forge/examples/sudoku_opt_viz/sudoku.js new file mode 100644 index 00000000..17db081e --- /dev/null +++ b/forge/examples/sudoku_opt_viz/sudoku.js @@ -0,0 +1,62 @@ +d3 = require('d3') +d3.selectAll("svg > *").remove(); + +function printValue(row, col, yoffset, value) { + d3.select(svg) + .append("text") + .style("fill", "black") + .attr("x", row*25) + .attr("y", col*26 + yoffset) + .text(value); +} + +const rows = 9 +const cols = 9 + +function printBoard(boardAtom, yoffset) { + for (r = 1; r <= rows; r++) { + for (c = 1; c <= cols; c++) { + printValue(r, c, yoffset, + boardAtom.board[r][c] + .toString().substring(0,1)) + } + } + + d3.select(svg) + .append('rect') + .attr('x', 10) + .attr('y', yoffset+7) + .attr('width', 240) + .attr('height', 240) + .attr('stroke-width', 3) + .attr('stroke', 'black') + .attr('fill', 'transparent'); + + for (x = 1; x<3; x++) { + d3.select(svg) + .append('line') + .attr('x1', 10+x*(240/3)) + .attr('y1', yoffset+7) + .attr('x2', 10+x*(240/3)) + .attr('y2', 250+yoffset) + .attr('stroke-width', 1) + .attr('stroke', 'black') + .attr('fill', 'transparent'); + + d3.select(svg) + .append('line') + .attr('x1', 10) + .attr('y1', yoffset+5+x*(240/3)) + .attr('x2', 250) + .attr('y2', yoffset+5+x*(240/3)) + .attr('stroke-width', 1) + .attr('stroke', 'black') + .attr('fill', 'transparent'); + + } + + +} + +printBoard(BoardState.atom("PuzzleState0"), 0) +printBoard(BoardState.atom("SolvedState0"), 240) diff --git a/forge/examples/sudoku_opt_viz/sudoku_basic.frg b/forge/examples/sudoku_opt_viz/sudoku_basic.frg new file mode 100644 index 00000000..24bcc754 --- /dev/null +++ b/forge/examples/sudoku_opt_viz/sudoku_basic.frg @@ -0,0 +1,110 @@ +#lang forge + +/* + Example for exploring various optimizations + VERSION 1: a first try +*/ + +abstract sig BoardState { + board: pfunc Int -> Int -> Int +} +one sig PuzzleState extends BoardState {} +one sig SolvedState extends BoardState {} + +pred wellformed { + -- No <= 0 or >9 values used for indexing or values + all s: BoardState | + all i: Int | (i <= 0 or i > 9) implies { + no s.board[i] + no s.board[Int][i] + no s.board.i + } +} + + +fun get_grid[s: BoardState, row_offset, col_offset: Int]: set Int { + let rows = row_offset + add[row_offset, 1] + add[row_offset, 2] | + let cols = col_offset + add[col_offset, 1] + add[col_offset, 2] | + s.board[rows][cols] +} + +fun values: set Int { + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 +} + +pred solution[s: BoardState] { + -- ** Rows and Columns ** + -- don't use #... = 9 here; instead something like: + all r: values | s.board[r][Int] = values + all c: values | s.board[Int][c] = values + -- note this is a situation where the relational perspective can + -- help make your constraints more readable, rather than less so. + + -- ** Subgrids ** + all row_offset, col_offset: (1 + 4 + 7) | + get_grid[s, row_offset, col_offset] = values + +} + +pred solve { + PuzzleState.board in SolvedState.board + solution[SolvedState] +} + +/* + #vars: (size-variables 458692); #primary: (size-primary 65536); #clauses: (size-clauses 1399152) + Transl (ms): (time-translation 4527); Solving (ms): (time-solving 26934) +*/ +/*run { + wellformed + solve + #PuzzleState.board = 7 // 7 pre-populated cells +} for 2 BoardState, 5 Int +*/ + +/* You might think the core problem is wellformed: we dont NEED + those constraints; we can just ignore entries outside [1,9] + Unfortunately: +#vars: (size-variables 457409); #primary: (size-primary 65536); #clauses: (size-clauses 1256181) +Transl (ms): (time-translation 4062); Solving (ms): (time-solving 1901) +*/ +/*run { + -- without wellformed + solve + #PuzzleState.board = 7 // 7 pre-populated cells +} for 2 BoardState, 5 Int +*/ + +/* + This *would* be more efficient if you were willing to use + 4 Int (the interval [-7, 8]) and translate in the visualizer. + but that increases complexity of the model and makes it harder + to understand. What we can do instead is tell the translation + process that the `board` relation can't use any negative indexes + or contain negative values. +*/ + +/* + Let's try solving a "hard" Sudoku puzzle + +#vars: (size-variables 232156); #primary: (size-primary 65536); #clauses: (size-clauses 367445) +Transl (ms): (time-translation 1815); Solving (ms): (time-solving 645) + +*/ +pred puzzle1 { + PuzzleState.board = + (1 -> 1 -> 6) + (1 -> 4 -> 9) + (1 -> 9 -> 8) + + (2 -> 7 -> 4) + (2 -> 8 -> 3) + + (3 -> 1 -> 1) + (3 -> 5 -> 4) + (3 -> 8 -> 9) + + (4 -> 1 -> 5) + (4 -> 4 -> 8) + (4 -> 9 -> 7) + + (6 -> 2 -> 1) + (6 -> 6 -> 2) + (6 -> 9 -> 9) + + (7 -> 2 -> 7) + (7 -> 4 -> 5) + (7 -> 9 -> 1) + + (8 -> 2 -> 3) + (8 -> 4 -> 4) + + (9 -> 2 -> 2) + (9 -> 5 -> 8) + (9 -> 7 -> 7) + (9 -> 9 -> 3) +} + +run { + solve + puzzle1 +} for 2 BoardState, 5 Int + diff --git a/forge/examples/sudoku_opt_viz/sudoku_rethink.frg b/forge/examples/sudoku_opt_viz/sudoku_rethink.frg new file mode 100644 index 00000000..8a1eeb2b --- /dev/null +++ b/forge/examples/sudoku_opt_viz/sudoku_rethink.frg @@ -0,0 +1,129 @@ +#lang forge + +/* + Example for exploring various optimizations + VERSION 4: rethinking the model + + Pure SAT is known to solve hard sudoku puzzles in 10-100ms. + We're taking an order of magnitude longer than we should be! + Let's try a different way of encoding the problem: only *one* board. +*/ + +one sig Board { + board: pfunc Int -> Int -> Int +} + +-- There are 9 subgrids; define them as constants +fun subgrids: set Int -> Int -> Int { + (1 -> (1 + 2 + 3) -> (1 + 2 + 3)) + + (2 -> (1 + 2 + 3) -> (4 + 5 + 6)) + + (3 -> (1 + 2 + 3) -> (7 + 8 + 9)) + + (4 -> (4 + 5 + 6) -> (1 + 2 + 3)) + + (5 -> (4 + 5 + 6) -> (4 + 5 + 6)) + + (6 -> (4 + 5 + 6) -> (7 + 8 + 9)) + + (7 -> (7 + 8 + 9) -> (1 + 2 + 3)) + + (8 -> (7 + 8 + 9) -> (4 + 5 + 6)) + + (9 -> (7 + 8 + 9) -> (7 + 8 + 9)) +} + +fun values: set Int { + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) +} + +fun get_grid[subgrid: Int]: set Int { + let indexes = subgrids[subgrid] | + let rows = indexes.Int | + let cols = indexes[Int] | + Board.board[rows][cols] +} + +pred solution { + + -- ** Rows and Columns ** + -- don't use #... = 9 here; instead something like: + all r: values | Board.board[r][Int] = values + all c: values | Board.board[Int][c] = values + -- note this is a situation where the relational perspective can + -- help make your constraints more readable, rather than less so. + + -- ** Subgrids ** + all subgrid: values | + get_grid[subgrid] = values + +} + +inst optimizer_puzzle1 { + Board = `Board0 + + -- There's a small additional chance for optimization here, but + -- it seems like a lot of work: RELATIONS are a problem here! + -- The upper bound is too big---unaware of the fact that nothing + -- else can co-exist in the cells we already have values for. + + -- UPPER BOUND + board in + (Board -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9)) + + -- LOWER BOUND + board ni + (Board -> + ((1 -> 1 -> 6) + (1 -> 4 -> 9) + (1 -> 9 -> 8) + + (2 -> 7 -> 4) + (2 -> 8 -> 3) + + (3 -> 1 -> 1) + (3 -> 5 -> 4) + (3 -> 8 -> 9) + + (4 -> 1 -> 5) + (4 -> 4 -> 8) + (4 -> 9 -> 7) + + (6 -> 2 -> 1) + (6 -> 6 -> 2) + (6 -> 9 -> 9) + + (7 -> 2 -> 7) + (7 -> 4 -> 5) + (7 -> 9 -> 1) + + (8 -> 2 -> 3) + (8 -> 4 -> 4) + + (9 -> 2 -> 2) + (9 -> 5 -> 8) + (9 -> 7 -> 7) + (9 -> 9 -> 3))) +} + +/* + Interestingly, even this small change -- one board only -- helps + + #vars: (size-variables 2296); #primary: (size-primary 706); #clauses: (size-clauses 2786) + Transl (ms): (time-translation 244); Solving (ms): (time-solving 758) + + It's possible some of this is setup/teardown cost for the solver or + the translation infrastructure. But process startup shouldn't be + included. So this still seems quite high. +*/ +/* +run { + solution +} for 1 Board, 5 Int for optimizer_puzzle1 +*/ +/* + Let's try a different way to express the problem: + +#vars: (size-variables 5292); #primary: (size-primary 706); #clauses: (size-clauses 7155) +Transl (ms): (time-translation 330); Solving (ms): (time-solving 153) + + The problem got bigger---in terms of clauses. But the solver + had much more luck solving it. + + What's the lesson here? While smaller problems are *often* better, especially + for the translation time, an encoding with more clauses can give the solver + the structure it needs to solve the problem more efficiently. Don't be afraid + to try different ways of expressing your goal. +*/ + +pred solution2 { + -- There is an entry in every cell + -- (In a separate file, this would just mean changing the type + -- of board to func, rather than pfunc) + all r, c: values | some Board.board[r][Int] + -- Each row and col contain at most one of every value + all val, r: values | lone c : values | Board.board[r][c] = val + all val, c: values | lone r : values | Board.board[r][c] = val + + all subgrid, val: values | val in get_grid[subgrid] + +} +run { + solution2 +} for 1 Board, 5 Int for optimizer_puzzle1 + + diff --git a/forge/examples/sudoku_opt_viz/sudoku_unrolled.frg b/forge/examples/sudoku_opt_viz/sudoku_unrolled.frg new file mode 100644 index 00000000..0e5e6221 --- /dev/null +++ b/forge/examples/sudoku_opt_viz/sudoku_unrolled.frg @@ -0,0 +1,189 @@ +#lang forge + +/* + Example for exploring various optimizations + VERSION 3: extending the optimizer instance a bit +*/ + +abstract sig BoardState { + board: pfunc Int -> Int -> Int +} +one sig PuzzleState extends BoardState {} +one sig SolvedState extends BoardState {} + +inst optimizer { + -- Just 2 board states (don't name the atoms the same as the sigs) + PuzzleState = `PuzzleState0 + SolvedState = `SolvedState0 + BoardState = PuzzleState + SolvedState + -- Upper-bound on the board relation: don't even try to use + -- a row, column, or value that's outside the interval [1, 9] + board in BoardState -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) +} + +-- There are 9 subgrids; define them as constants +fun subgrids: set Int -> Int -> Int { + (1 -> (1 + 2 + 3) -> (1 + 2 + 3)) + + (2 -> (1 + 2 + 3) -> (4 + 5 + 6)) + + (3 -> (1 + 2 + 3) -> (7 + 8 + 9)) + + (4 -> (4 + 5 + 6) -> (1 + 2 + 3)) + + (5 -> (4 + 5 + 6) -> (4 + 5 + 6)) + + (6 -> (4 + 5 + 6) -> (7 + 8 + 9)) + + (7 -> (7 + 8 + 9) -> (1 + 2 + 3)) + + (8 -> (7 + 8 + 9) -> (4 + 5 + 6)) + + (9 -> (7 + 8 + 9) -> (7 + 8 + 9)) +} + +fun values: set Int { + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) +} + +fun get_grid[s: BoardState, subgrid: Int]: set Int { + let indexes = subgrids[subgrid] | + let rows = indexes.Int | + let cols = indexes[Int] | + s.board[rows][cols] +} + +pred solution[s: PuzzleState] { + -- ** Rows and Columns ** + -- don't use #... = 9 here; instead something like: + all r: values | s.board[r][Int] = values + all c: values | s.board[Int][c] = values + -- note this is a situation where the relational perspective can + -- help make your constraints more readable, rather than less so. + + -- ** Subgrids ** + all subgrid: values | + get_grid[s, subgrid] = values + +} + +pred solve { + PuzzleState.board in SolvedState.board + solution[SolvedState] +} + + +/* + +Old optimizer: + #vars: (size-variables 10943); #primary: (size-primary 1458); #clauses: (size-clauses 29422) + Transl (ms): (time-translation 472); Solving (ms): (time-solving 6321) +New (with grids): + #vars: (size-variables 10943); #primary: (size-primary 1458); #clauses: (size-clauses 29422) + Transl (ms): (time-translation 271); Solving (ms): (time-solving 3146) + +Notice that the problem size is still the same. Why? +If I had to guess, I'd say that perhaps Forge handled the arithmetic +in the translation process. That time did decrease. But it's tough +to rely on timing like this, since it's not always deterministic. +To be honest, I'm not immediately sure why the solving time also +decreased. I think this is a better way of encoding the "neighborhood" +of each cell, regardless---since there's less risk of solver impact. +*/ + +/*run { + solve + #PuzzleState.board = 7 // 7 pre-populated cells +} for 2 BoardState, 5 Int for optimizer +*/ +/* + Let's try solving a "hard" Sudoku puzzle +Basic version was: + #vars: (size-variables 232156); #primary: (size-primary 65536); #clauses: (size-clauses 367445) + Transl (ms): (time-translation 1815); Solving (ms): (time-solving 645) +Now: + #vars: (size-variables 5483); #primary: (size-primary 1458); #clauses: (size-clauses 7993) + Transl (ms): (time-translation 318); Solving (ms): (time-solving 1708) + +Note that even though the time-to-solve is comparable, the work has shifted +from the translation to the solver. + +*/ +pred puzzle1 { + PuzzleState.board = + (1 -> 1 -> 6) + (1 -> 4 -> 9) + (1 -> 9 -> 8) + + (2 -> 7 -> 4) + (2 -> 8 -> 3) + + (3 -> 1 -> 1) + (3 -> 5 -> 4) + (3 -> 8 -> 9) + + (4 -> 1 -> 5) + (4 -> 4 -> 8) + (4 -> 9 -> 7) + + (6 -> 2 -> 1) + (6 -> 6 -> 2) + (6 -> 9 -> 9) + + (7 -> 2 -> 7) + (7 -> 4 -> 5) + (7 -> 9 -> 1) + + (8 -> 2 -> 3) + (8 -> 4 -> 4) + + (9 -> 2 -> 2) + (9 -> 5 -> 8) + (9 -> 7 -> 7) + (9 -> 9 -> 3) +} +// run { +// solve +// puzzle1 +// } for 2 BoardState, 5 Int for optimizer + +/* + We'd expect 9*9*9=729 variables per board. We've got 1458 for + 2 boards (one is fully defined, but not via bounds). That's + exactly what we'd expect. If it wasn't, we could investigate + by looking at the bounds passed to the solver via `option verbose`. + + But wait---why do we have variables for the first board at all? + Because `puzzle` is a predicate. Ideally, we'd give it as a bound + via `inst`. But this is challenging: + * the PuzzleState's board is known exactly; but + * the SolvedState's board is only UPPER bounded. + We can solve this in a few ways. Here's one: +*/ + + +inst optimizer_puzzle1 { + -- Just 2 board states (don't name the atoms the same as the sigs) + PuzzleState = `PuzzleState0 + SolvedState = `SolvedState0 + BoardState = PuzzleState + SolvedState + + -- UPPER BOUND + board in + -- flexible for SolvedState, but on interval [1,9]: + (SolvedState -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9)) + + + -- fully known for PuzzleState: + (PuzzleState -> + ((1 -> 1 -> 6) + (1 -> 4 -> 9) + (1 -> 9 -> 8) + + (2 -> 7 -> 4) + (2 -> 8 -> 3) + + (3 -> 1 -> 1) + (3 -> 5 -> 4) + (3 -> 8 -> 9) + + (4 -> 1 -> 5) + (4 -> 4 -> 8) + (4 -> 9 -> 7) + + (6 -> 2 -> 1) + (6 -> 6 -> 2) + (6 -> 9 -> 9) + + (7 -> 2 -> 7) + (7 -> 4 -> 5) + (7 -> 9 -> 1) + + (8 -> 2 -> 3) + (8 -> 4 -> 4) + + (9 -> 2 -> 2) + (9 -> 5 -> 8) + (9 -> 7 -> 7) + (9 -> 9 -> 3))) + + -- LOWER BOUND + board ni + -- both PuzzleState and SolvedState need to contain these: + (BoardState -> + ((1 -> 1 -> 6) + (1 -> 4 -> 9) + (1 -> 9 -> 8) + + (2 -> 7 -> 4) + (2 -> 8 -> 3) + + (3 -> 1 -> 1) + (3 -> 5 -> 4) + (3 -> 8 -> 9) + + (4 -> 1 -> 5) + (4 -> 4 -> 8) + (4 -> 9 -> 7) + + (6 -> 2 -> 1) + (6 -> 6 -> 2) + (6 -> 9 -> 9) + + (7 -> 2 -> 7) + (7 -> 4 -> 5) + (7 -> 9 -> 1) + + (8 -> 2 -> 3) + (8 -> 4 -> 4) + + (9 -> 2 -> 2) + (9 -> 5 -> 8) + (9 -> 7 -> 7) + (9 -> 9 -> 3))) +} + +/* + Better (in terms of problem size): +#vars: (size-variables 2296); #primary: (size-primary 706); #clauses: (size-clauses 2786) +Transl (ms): (time-translation 528); Solving (ms): (time-solving 1869) + + But still not really ideal! There's a lot of branching happening. + + +*/ + +run { + solve +} for 2 BoardState, 5 Int for optimizer_puzzle1 diff --git a/forge/examples/sudoku_opt_viz/sudoku_with_inst.frg b/forge/examples/sudoku_opt_viz/sudoku_with_inst.frg new file mode 100644 index 00000000..60fd7558 --- /dev/null +++ b/forge/examples/sudoku_opt_viz/sudoku_with_inst.frg @@ -0,0 +1,90 @@ +#lang forge + +/* + Example for exploring various optimizations + VERSION 2: adding an optimizer instance for `board` +*/ + +abstract sig BoardState { + board: pfunc Int -> Int -> Int +} +one sig PuzzleState extends BoardState {} +one sig SolvedState extends BoardState {} + +pred wellformed { + -- No <= 0 or >9 values used for indexing or values + all s: BoardState | + all i: Int | (i <= 0 or i > 9) implies { + no s.board[i] + no s.board[Int][i] + no s.board.i + } +} + +inst optimizer { + -- Just 2 board states (don't name the atoms the same as the sigs) + PuzzleState = `PuzzleState0 + SolvedState = `SolvedState0 + BoardState = PuzzleState + SolvedState + -- Upper-bound on the board relation: don't even try to use + -- a row, column, or value that's outside the interval [1, 9] + board in BoardState -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) + +} + +fun get_grid[s: BoardState, row_offset, col_offset: Int]: set Int { + let rows = row_offset + add[row_offset, 1] + add[row_offset, 2] | + let cols = col_offset + add[col_offset, 1] + add[col_offset, 2] | + s.board[rows][cols] +} + +fun values: set Int { + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 +} + +pred solution[s: PuzzleState] { + -- ** Rows and Columns ** + -- don't use #... = 9 here; instead something like: + all r: values | s.board[r][Int] = values + all c: values | s.board[Int][c] = values + -- note this is a situation where the relational perspective can + -- help make your constraints more readable, rather than less so. + + -- ** Subgrids ** + all row_offset, col_offset: (1 + 4 + 7) | + get_grid[s, row_offset, col_offset] = values + +} + +pred solve { + PuzzleState.board in SolvedState.board + solution[SolvedState] +} + +/* +Just by adding the optimizer partial instance, we see: +#vars: (size-variables 11096); #primary: (size-primary 1458); #clauses: (size-clauses 29422) +Transl (ms): (time-translation 356); Solving (ms): (time-solving 10463) +* major reduction in problem size +* >2 performance improvement: ~30sec -> ~11sec. +*/ +run { + wellformed + solve + #PuzzleState.board = 7 // 7 pre-populated cells +} for 2 BoardState, 5 Int for optimizer + +/* + We don't even need wellformedness anymore, if we're using optimizer + +#vars: (size-variables 10943); #primary: (size-primary 1458); #clauses: (size-clauses 29422) +Transl (ms): (time-translation 472); Solving (ms): (time-solving 6321) + +*/ +run { + solve + #PuzzleState.board = 7 // 7 pre-populated cells +} for 2 BoardState, 5 Int for optimizer diff --git a/forge/examples/sudoku_opt_viz/sudoku_with_inst_2.frg b/forge/examples/sudoku_opt_viz/sudoku_with_inst_2.frg new file mode 100644 index 00000000..779df0d4 --- /dev/null +++ b/forge/examples/sudoku_opt_viz/sudoku_with_inst_2.frg @@ -0,0 +1,104 @@ +#lang forge + +/* + Example for exploring various optimizations + VERSION 3: extending the optimizer instance a bit +*/ + +-- Pre-load the visualizer script in Sterling +option run_sterling "sudoku.js" +-- For ease of debugging and demoing, use a constant Forge server port +option sterling_port 17100 + + +abstract sig BoardState { + board: pfunc Int -> Int -> Int +} +one sig PuzzleState extends BoardState {} +one sig SolvedState extends BoardState {} + +-- Useful way to add helper relations +one sig Helper { + -- encode the set of values in bounds, not constraints + values: set Int +} + +inst optimizer { + -- Just 2 board states (don't name the atoms the same as the sigs) + PuzzleState = `PuzzleState0 + SolvedState = `SolvedState0 + BoardState = PuzzleState + SolvedState + -- Upper-bound on the board relation: don't even try to use + -- a row, column, or value that's outside the interval [1, 9] + board in BoardState -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) -> + (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) + + -- encode the set of values in bounds, not constraints + Helper = `Helper0 + values = Helper -> (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9) +} + +fun get_grid[s: BoardState, row_offset, col_offset: Int]: set Int { + let rows = row_offset + add[row_offset, 1] + add[row_offset, 2] | + let cols = col_offset + add[col_offset, 1] + add[col_offset, 2] | + s.board[rows][cols] +} + +pred solution[s: PuzzleState] { + -- ** Rows and Columns ** + -- don't use #... = 9 here; instead something like: + all r: Helper.values | s.board[r][Int] = Helper.values + all c: Helper.values | s.board[Int][c] = Helper.values + -- note this is a situation where the relational perspective can + -- help make your constraints more readable, rather than less so. + + -- ** Subgrids ** + all row_offset, col_offset: (1 + 4 + 7) | + get_grid[s, row_offset, col_offset] = Helper.values + +} + +pred solve { + PuzzleState.board in SolvedState.board + solution[SolvedState] +} + + +/* + IN THIS CASE, we don't even need wellformedness anymore, + if we're using optimizer. Normally, I'd keep the wellformed + predicate around (because it's not always the case that + we want to use optimizer for all runs/tests). + +Old optimizer: + #vars: (size-variables 10943); #primary: (size-primary 1458); #clauses: (size-clauses 29422) + Transl (ms): (time-translation 472); Solving (ms): (time-solving 6321) +New optimizer: + #vars: (size-variables 10943); #primary: (size-primary 1458); #clauses: (size-clauses 29422) + Transl (ms): (time-translation 445); Solving (ms): (time-solving 5370) + +Interesting! The bounds aren't helping reduce the size of the problem. +Forge already had the constant (1 + ... + 9) in place. +*/ +run { + solve + #PuzzleState.board = 7 // 7 pre-populated cells +} for 2 BoardState, 5 Int for optimizer + +/* + The "#PuzzleState.board = 7" is far more suspicious. Cardinality + is expensive to encode into SAT, and 7 is fairly high. Just how much + of the translation and solving time is due to the "populate + exactly 7 squares in the puzzle" constraint? + + #vars: (size-variables 5480); #primary: (size-primary 1458); #clauses: (size-clauses 7261) + Transl (ms): (time-translation 225); Solving (ms): (time-solving 6747) + + The problem got simpler, but the solver time went up. :-( +*/ +run { + solve + --#PuzzleState.board = 7 +} for 2 BoardState, 5 Int for optimizer diff --git a/forge/examples/tic_tac_toe_assertions.frg b/forge/examples/tic_tac_toe/tic_tac_toe_assertions.frg similarity index 100% rename from forge/examples/tic_tac_toe_assertions.frg rename to forge/examples/tic_tac_toe/tic_tac_toe_assertions.frg diff --git a/forge/examples/ttt_viz.js b/forge/examples/tic_tac_toe/ttt_viz.js similarity index 100% rename from forge/examples/ttt_viz.js rename to forge/examples/tic_tac_toe/ttt_viz.js diff --git a/forge/examples/unsat/README.md b/forge/examples/unsat/README.md new file mode 100644 index 00000000..3cc1fae6 --- /dev/null +++ b/forge/examples/unsat/README.md @@ -0,0 +1,3 @@ +# Unsatisfiable Cores + +These examples illustrate various kinds of unsat core behavior in Forge. Begin with `unsat_example.frg`, as it more completely documents the settings used. diff --git a/forge/examples/unsat/unsat_big.frg b/forge/examples/unsat/unsat_big.frg new file mode 100644 index 00000000..5e370aa4 --- /dev/null +++ b/forge/examples/unsat/unsat_big.frg @@ -0,0 +1,27 @@ +#lang forge/temporal +/* + This model documents a place that Forge disagrees with Alloy. + Pardinus applies a rewriting process to convert temporal formulas + to normal formulas referencing "timed" relations. Usually, these + rewrites are included in the mapping back to original formulas + that cores rely on. Here, however, one is not: an "extra" formula + gets produced that has no attached location. + + In Alloy, this model will not produce a core at all. + In Forge, it produces a core, with one "extra" formula + unattributed. This is expressed via an "[UNKNOWN]" annotation, + and then Forge prints the formula to console. + + (as of May 2024 -- TN) + +*/ + +option run_sterling off + +option solver MiniSatProver +option core_minimization rce +option logtranslation 1 +option coregranularity 1 +sig Post {} +sig Server {var posts : set Post } +test expect {{ (posts)' != (posts)' } is unsat } diff --git a/forge/examples/unsat/unsat_comprehension.frg b/forge/examples/unsat/unsat_comprehension.frg new file mode 100644 index 00000000..f74317b2 --- /dev/null +++ b/forge/examples/unsat/unsat_comprehension.frg @@ -0,0 +1,17 @@ +#lang forge/temporal + +option solver MiniSatProver +option core_minimization rce +option logtranslation 1 +option coregranularity 1 +option verbose 5 + +sig Node {edges: set Node} + +run { + no Node + some { + n1: Node | some n1 + } +} + diff --git a/forge/examples/unsat/unsat_example.frg b/forge/examples/unsat/unsat_example.frg new file mode 100644 index 00000000..f33b7990 --- /dev/null +++ b/forge/examples/unsat/unsat_example.frg @@ -0,0 +1,46 @@ +#lang forge + +/* + (Last updated in May 2024) + + Example of unsat-core highlighting in Forge. It's important that you're running + Forge 3.4 or later with the latest VSCode extension to get highlighting. It's also + important to keep in mind that there are corner cases where the core will contain + formulas that are not mapped to a location in the model. This is rare, but happens + in Alloy, too. (Alloy will not give a core at all in these cases; Forge will print + a combination of: + (1) locations in the source; AND + (2) constraints that aren't directly mapped back.) + + If you're using the VSCode extension, a core will be underlined in red. + If you're _not_ using the VSCode extension, you'll see the location info in the terminal. + + NOTE WELL: if you're running in VSCode, you may need to click "continue" to see the core + for a "run" command. +*/ + +---------------------------------------------------------------------------------- +-- Manually enable core extraction (see docs for more information than below) +option solver MiniSatProver -- the only solver we support that extracts cores +option logtranslation 2 -- enable translation logging (1 = faster, less fine-grained) +option coregranularity 2 -- how fine-grained cores should be (1 = faster, less fine-grained) +option core_minimization rce -- tell the solver which algorithm to use to reduce core size + -- valid values: hybrid (fast, not always minimal), + -- rce (slower, complete) +---------------------------------------------------------------------------------- + +sig Node {edges: set Node} +test expect { + -- This run has multiple potential cores. At least two: + -- Core A: the "no edges" mixed with the "n1->n2" + -- Core B: the "no edges" mixed with the "n2->n1". + -- Both will also highlight the variables involved; notice that "n3" is not blamed. + complexUnsat: { + some n1, n2, n3: Node | { + n1->n2 in edges + n2->n1 in edges + n3 not in n3.edges + } + no edges + } is unsat +} diff --git a/forge/examples/unsat/unsat_example.png b/forge/examples/unsat/unsat_example.png new file mode 100644 index 00000000..f3b2859a Binary files /dev/null and b/forge/examples/unsat/unsat_example.png differ diff --git a/forge/examples/unsat/unsat_temporal.frg b/forge/examples/unsat/unsat_temporal.frg new file mode 100644 index 00000000..8b19399d --- /dev/null +++ b/forge/examples/unsat/unsat_temporal.frg @@ -0,0 +1,17 @@ +#lang forge/temporal +option min_tracelength 3 +option solver MiniSatProver +option core_minimization rce +option logtranslation 1 + +option max_tracelength 16 + +one sig World { + var counter: one Int +} + +pred init { World.counter = 0 } +pred step { World.counter' = add[World.counter, 1]} +test expect { + isUnsat: {init and always step and World.counter = 1} is unsat +} \ No newline at end of file diff --git a/forge/examples/unsat/unsat_temporal_no_var.frg b/forge/examples/unsat/unsat_temporal_no_var.frg new file mode 100644 index 00000000..d7ce4ab5 --- /dev/null +++ b/forge/examples/unsat/unsat_temporal_no_var.frg @@ -0,0 +1,23 @@ +#lang forge/temporal + +/* + As of May 2024, this model now gives an error, rather than producing + unsat. (The file previously tested behavior when unsat came from + lack of a "var" annotation on a field that needed to be variable.) +*/ + +option solver MiniSatProver +option core_minimization rce +option logtranslation 1 +option coregranularity 1 + +one sig World { + -- Forgot "var"! + counter: one Int +} + +pred init { World.counter = 0 } +pred step { World.counter' = subtract[World.counter, -1]} +test expect { + isUnsat: {init and always step} for 2 Int is forge_error // unsat +} \ No newline at end of file