Note the ./ in the install command! If you write raco pkg install forge froglet, that will install both from the package server instead of your local directory. Adding prefix ./ tells raco that you're talking about folders instead. It's also important to have both ./forge and ./froglet in the single command; they depend on each other, so leaving one out will cause raco to "helpfully" install it from the package server, not your local drive.

An early version of this extension was provided via Github, rather than the VSCode Marketplace. Please use the Marketplace version (and uninstall the other, if you have it) if for no other reason than it will automatically update when you restart VSCode.

We can draw a very rough analogy to object-oriented programming here. We might say:

• a sig definition, along with its fields, is like a class; and
• atoms within an instance of a model are like objects (since each atom belongs to some sig). This is a useful analogy!

Just remember that it is an analogy and not the exact truth. There are important differences. For example, you might remember the heap from Java or some other language, and wonder how atoms (analogously to objects) are created or garbage-collected. But there is no heap in Forge instances, only a set of atoms for each sig. Similarly, you might wonder how a Forge model executes. But it doesn't! A Forge model defines a set of possible instances, which the tool searches for.

You cannot use the same field name within two different sigs in a model. This is because field names are globally available for writing constraints.

Forge must have bounds for every sig, including child sigs. The default of 0-to-4 objects is applied to every top-level sig. Forge can often infer consistent bounds for child sigs, but it cannot always do so and will require you to provide them. This is most often the case in the presence of complex hierarchies involving abstract and one sigs.

More importantly, example and inst syntax require the contents of parent sigs to be defined once the contents of a single child are set. To see why, consider this example:

example workingCats is {myPredicate} for {
    ActorCat = `ActorCat0 + `ActorCat1
    ProgrammerCat = `ProgrammerCat0 + `ProgrammerCat1
}

This produces an error:

run: Please specify an upper bound for ancestors of ActorCat.

This error occurs because Forge knows only that there are 2 specific actors and 2 specific programmers, and can't infer whether any other cats exist. To fix the error, provide bounds for the parent sig:

example workingCats is {myPredicate} for {    
    ActorCat = `ActorCat0 + `ActorCat1
    ProgrammerCat = `ProgrammerCat0 + `ProgrammerCat1
    Cat = `ActorCat0 + `ActorCat1 + `ProgrammerCat0 + `ProgrammerCat1
}

Froglet does not support the set multiplicity, because sets add a layer of complexity to the language. If you really need to model sets in Froglet, you an approximate them using boolean-valued functions (see below).

Froglet does not support the set multiplicity, because sets add a layer of complexity to the language. If you really need to model sets in Froglet, you an approximate them using boolean-valued functions (see below).

If you are currently working in Froglet, you may see terms in this document that you aren't yet familiar with.

Unlike what would happen in a programming language like JavaScript or Python, attempting to use an expression in place of a formula, or vice versa, will produce an error in Forge when you try to run your model. For example, if we wrote the constraint all s: Student | s.grades, what would that mean? That every s exists? That every s has passed some class? Something different? To avoid this ambiguity, Forge doesn't try to infer your meaning, and just gives an error.

Always ask, for every word you write: are you writing about what must be true, or naming some atom or set of atoms?

If you are working in Froglet, the remainder of this page may reference terms you are as yet unfamiliar with. Don't worry; this will be covered more in class. Informally, you might read "relation" as "function".

</div>
</div>

## Formal Definition of Instances

Because `sig` definitions can involve concepts like inheritance, partial functions, and uniqueness, the precise definition is a bit involved.

Consider an arbitrary Forge model $M$ that defines some `sig`s and fields.

An _instance_ is a collection of finite sets for each `sig` and field in the model. For each `sig S` in the model, an instance contains a set $S$ where:
  - if `S` has a parent `sig P`, then the contents of $S$ must be a subset of the contents of $P$;
  - for any pair of child-sigs of `S`, `C1` and `C2`, $C_1$ and $C_2$ have no elements in common; 
  - if `S` is declared `abstract` and has child sigs, then any object in $S$ must also be present in $C$ for some `sig C` that extends `sig S`; and
  - if `S` is declared `one` or `lone`, then $S$ contains exactly one or at most one object, respectively.

For each field `f` of type `S1 -> ... -> Sn` of `sig S` in the model, an instance contains a set $f$ where:
  - $f$ is subset of the cross product $S\times S_1 \times ... \times S_N$;
  - if `f` is declared `one` or `lone`, then $f$ can only contain exactly one or at most one object, respectively;
  - if `f` is declared `func`, then there is exactly one entry in $f$ for each $(s, s_1, ..., s_{n-1})$ in $S\times S_1 \times ... \times S_{(n-1)}$.
  - if `f` is declared `pfunc`, then there is at most one entry in $f$ for each $(s, s_1, ..., s_{n-1})$ in $S\times S_1 \times ... \times S_{(n-1)}$.

The union over all `sig`-sets $S$ in an instance (including the built-in sig `Int`) is said to be the _universe_ of that instance.


<div id="admonition-fields-are-not-objects" class="admonition admonish-tip">
<div class="admonition-title">

Fields are not objects

<a class="admonition-anchor-link" href="#admonition-fields-are-not-objects"></a>
</div>
<div>

It is sometimes useful to use terminology from object-oriented programming to think about Forge models. For example, we can think of a `pfunc` field like a dictionary in Python or a map in Java. However, _a field is not an object_. This matters for at least two reasons:
- We can't write a constraint like "every `pfunc` field in the model is non-empty", because there's no set of `pfunc` "objects" to examine.
- Two different objects in an instance will be considered non-equal in Forge, even if they belong to the same `sig` and have identical field contents. In contrast, two fields themselves are equal in Forge if they have identical contents; fields are relations that involve atoms, not objects themselves.

</div>
</div>
  

<div id="admonition-tuples-arity" class="admonition admonish-info">
<div class="admonition-title">

Tuples, Arity

<a class="admonition-anchor-link" href="#admonition-tuples-arity"></a>
</div>
<div>

An ordered list of elements is called a _tuple_, and we'll sometimes use that term to refer to elements of the `sig` and field sets in an instance. The number of elements in a tuple is called its _arity_. Since any single `sig` or field set will contain tuples with the same arity, we can safely talk about the arity of these sets as well. E.g., in the above definition, a field `f` of type `S1 -> ... -> Sn` in `sig S` would always correspond to a set with arity $n+1$.

</div>
</div>

Formulas

Formulas are a type of Forge syntax. Given an instance, every formula evaluates to a boolean value. If the formula is true of an instance, we say that the instance satisfies the formula.

Formula-Combining Operators

Formula operators combine smaller formulas to produce new formulas. Many closely resemble similar operators from programming languages, like &&, ||, and !.

List of Available Operators:

For the following <fmla> means an arbitrary formula.

• Negation: not (!)
• Conjunction: and (&&)
• Disjunction: or (||)
• Implication: implies (=>)
  • If-then-else: else
• If-and-only-if: iff (<=>)

not (alt: !)

not <fmla>

! <fmla>

true when <fmla> evaluates to false

and (alt: &&)

<fmla-a> and <fmla-b>

<fmla-a> && <fmla-b>

true when both <fmla-a> and <fmla-b> evaluate to true.

{
  some p.spouse
  p.spouse != p
}

or (alt: ||)

<fmla-a> or <fmla-b>

<fmla-a> || <fmla-b>

true when either <fmla-a> is true or <fmla-b> evaluates to true.

implies (alt =>)

<fmla-a> implies <fmla-b>

<fmla-a> => <fmla-b>

true when either <fmla-a> evaluates to false or <fmla-b> evaluates to true.

implies else (alt: => else)

{<fmla-a> implies <fmla-b> else <fmla-c>}

{<fmla-a> => <fmla-b> else <fmla-c>}

takes the value of <fmla-b> when <fmla-a> evaluates to true, and takes the value of <fmla-c> otherwise.

iff (alt: <=>)

<fmla-a> iff <fmla-b>

<fmla-a> <=> <fmla-b>

true when <fmla-a> evaluates to true exactly when <fmla-b> evaluates to true.

Cardinality and Membership

The following operators produce formulas from smaller expression arguments:

• no <expr>: true when <expr> is empty
• lone <expr>: true when <expr> contains zero or one elements
• one <expr>: true when <expr> contains exactly one element
• some <expr>: true when <expr> contains at least one element
• <expr-a> in <expr-b>: true when <expr-a> is a subset of or equal to <expr-b>
• <expr-a> = <expr-b>: true when <expr-a> and <expr-b> contain exactly the same elements

Quantifiers

In the following, <x> is a variable, <expr> is an expression of arity 1, and <fmla> is a formula (that can use the variable <x>). You can quantify over a unary set in the following ways:

• some <x>: <expr> | { <fmla> }: true when <fmla> is true for at least one element in <expr>; and
• all <x>: <expr> | { <fmla> }: true when <fmla> is true for all elements in <expr>

If you want to quantify over several variables, you can also do the following:

• some <x>: <expr-a>, <y>: <expr-b> | { <fmla> }; or
• some <x>, <y>: <expr> | { <fmla> }.

The syntax is the same for other quantifiers, such as all.

Complex Quantifiers

Forge also provides 3 additional quantifiers, which encode somewhat richer constraints than the above:

• no <x>: <expr> | { <fmla> }: true when <fmla> is false for all elements in <expr>
• lone <x>: <expr> | { <fmla> }: true when <fmla> is true for zero or one elements in <expr>
• one <x>: <expr> | { <fmla> }: true when <fmla> is true for exactly one element in <expr>

The above 3 quantifiers (no, lone, and one) should be used carefully. Because they invisibly encode extra constraints, they do not commute the same way some and all quantifiers do. E.g., some x : A | some y : A | myPred[x,y] is always equivalent to some y : A | some x : A | myPred[x,y], but one x : A | one y : A | myPred[x,y] is NOT always equivalent to one y : A | one x : A | myPred[x,y]. (Why not? Try it out in Forge!)

Quantifying Over Disjoint Objects

Sometimes, it might be useful to try to quantify over all pairs of elements in A, where the two in the pair are distinct atoms. You can do that using the disj keyword, e.g.:

• some disj x, y : A | ... (adds an implicit x != y and ...); and
• all disj x, y : A | ... (adds an implicit x != y implies ...)`

Predicates

If you have a set of constraints that you use often, or that you'd like to give a name to, you can define a predicate using the pred keyword. A predicate has the following form:

pred <pred-name> {
   <fmla-1>
   <fmla-2>
   ...
   <fmla-n>
}

Newlines between formulas in a pred will be combined implicitly with ands, helping keep your predicates uncluttered. Predicates can also be defined with arguments, which will be evaluated via substitution. For instance, in a family-tree model, you could create:

pred parentOrChildOf[p1, p2: Person] {
  p2 = p1.parent1 or
  p2 = p1.parent2 or
  p1 = p2.parent1 or
  p1 = p2.parent1
}

and then write something like some p : Person | parentOrChildOf[Tim, p]. Predicates may be used like this anywhere a formula can appear.

Expressions

Given an instance, expressions in Forge evaluate to sets of atoms.

Froglet

In Froglet, expressions must always denote a single atom or the empty set (none). This matches the abstraction where fields are always either total (one, func) or partial (lone, pfunc) functions.

Relational Operators

Relational Operators produce expressions (not formulas) from other expressions.

sig City {
    roads: set City
}

List of Relational Expression Operators:

• + (union)
• - (set difference)
• & (intersection)
• . [] (relational join)
• -> (cross product)
• ~ (transpose)
• ^ (transitive closure)
• * (reflexive transitive closure)
• => else
• set comprehension

+ (union)

<expr-a> + <expr-b>

returns the union of the two exprs, i.e., the set containing all elements that are in either of the two exprs.

BrownCS.employees = BrownCS.faculty + BrownCS.staff

- (set difference)

<expr-a> - <expr-b>

returns the set difference of the two exprs, i.e., everything in expr-a that is not also in expr-b.

BrownCS.utaCandidates = Student - BrownCS.htaHires

& (intersection)

<expr-a> & <expr-b>

returns the intersection of the two exprs, i.e., all elements in both expr-a and expr-b.

BrownCS.canUseAIML = BrownCS.tookLinearAlgebra & BrownCS.tookProbability 

-> (cross product)

<expr-a> -> <expr-b>

returns the cross product of the two exprs.

sig City {
    roads: set City
}
one sig Providence, Pawtucket extends City {}

~ (transpose)

~<expr>

returns the transpose of <expr>, assuming it is has arity 2. (Attempting to use transpose on a different-arity relation will produce an error.)

sig City {
    roads: set City
}

Set Comprehension

A set-comprehension expression {x1: T1, ..., xn: Tn | <fmla>} evaluates to a set of arity-n tuples. A tuple of objects o1, ... on is in the set if and only if <fmla> is satisfied when x1 takes the value o1, etc.

{s: Student, i: Faculty | some c: Course | { some s.grades[c] and c.instructor = i} }

. and [] (relational join)

<expr-a> . <expr-b>

returns the relational join of the two exprs. It combines two relations by seeking out rows with common values in their rightmost and leftmost columns. Concretely, if A is an $n$-ary relation, and B is $m$-ary, then A.B equals the $n+m-2$-ary relation:

$$\{a_1,...,a_{n-1},b_2,...,b_m|\exists x|(a_1,...,a_{n-1},x)\in A\text{ and }(x,b_2,...,b_m)\in B\}$$

sig City {
    roads: set City
}
one sig Providence extends City {}

inst joinExample {
    City = `Providence + `City0 + `City2
    roads = `Providence -> `City0 +
            `City0 -> `City1 +
            `City1 -> Providence
}

`Providence -> `City1   (because `Providence -> `City0 and `City0 -> `City1)
`City0 -> `Providence (because `City0 -> `City1 and `City1 -> `Providence)
`City1 -> `City0 (because `City1 -> `Providence and `Providence -> `City0)

`City0 (because `Providence -> `City0)

Alternative syntax: <expr-a>[<expr-b>]: is equivalent to <expr-b> . <expr-a>;

^ (transitive closure)

^<expr>

returns the transitive closure of <expr>, assuming it is has arity 2. Attempting to apply ^ to a relation of different arity will produce an error. The transitive closure of a binary relation $r$ is defined as the smallest relation $t$ such that:

• r in t; and
• for all a, b, and c, if a->b is in t and b->c is in t, then a->c is in t.

Informally, it is useful to think of ^r as encoding reachability using r. It is equivalent to the (unbounded and thus inexpressible in Forge) union: r + r.r + r.r.r + r.r.r.r + ....

sig City {
    roads: set City
}
one sig Providence extends City {}

* (reflexive transitive closure)

*<expr>

returns the reflexive-transitive closure of <expr>, assuming it is has arity 2. Attempting to apply * to a relation of different arity will produce an error.

For a given 2-ary relation r, *r is equivalent to ^r + iden.

if then else

{<fmla> => <expr-a> else <expr-b>}

returns <expr-a> if <fmla> evaluates to true, and <expr-b> otherwise.

Caveats: Alloy support

Forge does not currently support the relational Alloy operators <:, :>, or ++; if your models require them, please contact the Forge team.

Functions

In the same way that predicates define reusable formulas, functions define reusable expressions in Relational and Temporal Forge. Define functions with the fun keyword:

fun <fun-name>[<args>]: <result-type> {
   <expr>
}

fun inLawA[p: Person]: one Person {
  p.spouse.parent1
}

As with predicates, arguments will be evaluated via substitution. Functions may be used (with appropriate arguments) anywhere expressions can appear.

all p: Person | some inLawA[p]

all p: Person | some (p.spouse.parent1)

Let-Expressions

You can bind an expression to an identifier locally by using a let form:

let <id> = <expression> |
  <formula>

This is useful to avoid code bloat due to re-use. E.g., if s is a state:

let s2 = Traces.nextState[s] |
  canTransition[s, s2]

Using let in the evaluator

A let expression can be useful when debugging a model using Sterling's evaluator. E.g., if you want to evaluate an internal subformula for a specific value of a quantifier:

some p: Person | some p.spouse

you can check individual values by directly substituting (e.g., some Person0.spouse) but this is tiresome if the variable is used in multiple places. Instead, consider using let:

let p = Person0 | some p.spouse

Comments

Forge models support 3 different syntactic styles of comment:

• lines beginning with -- are ignored;
• lines beginning with // are ignored; and
• all text between /* and */ are ignored.

/*
/*
*/
*/

Running

There are two primary ways of running your spec. You can either as Forge to show you instances that satisfy a predicate you wrote with the run command, or ask Forge to look for counterexamples to a predicate you wrote with the check command.

Run

The run command can be used in a few different ways, show below:

<run-name>: run <pred> for <bounds>
<run-name>: run { <expr> } for <bounds>

Note that the run-name is optional to provide, but is helpful to distinguish what different run commands are showing.

When using the run command, Forge will display possible worlds (instances) where the predicates or expressions you specified evaluate to true, within the given bounds. Instances are displayed in Sterling If no such instances are found, "UNSAT" is displayed.

When no more satisfying instances can be found, Sterling displays "No more instances found".

Check

The check command is used to ask Forge to look for counterexamples to a given set of predicates, i.e. instances where the predicate or expression evaluates to false. The syntax is the same as for the run command, just with the keyword check instead:

<check-name>: check <pred> for <bounds>
<check-name>: check { <expr> } for <bounds>

If no counterexamples are found, Sterling displays "No counterexamples found. Assertion may be valid". When no more counterexamples can be found, Sterling displays "No more instances found".

Visualizing and Evaluating Output

Forge uses a modified version of the Sterling model visualizer.

Visualizing Output

When you execute your model, Forge will either look for instances that satisfy the predicates you wrote, or look for counterexamples to the assertion you wrote. If you used a run command, or if Forge found a counter-example to a test, example, or assert you wrote, Forge launches a window in your browser that displays the output. (See the run and check sections for the different displays Sterling has in various scenarios.)

The basic visualization of the model is a directed graph showing all the atoms in that instance and the relations between them. You can also view an alternate depiction of the instance in the table view tab. To keep visualizations neat, Sterling will not show you any Int atoms that are not used in the instance.

Theming

The directed-graph view can be customized by clicking the Theme tray to the right of the Sterling window. Sterling supports two kinds of theming, listed below.

Projections

Projecting over a sig hides atoms of that sig in the visualizer and shows the rest of the instance as if that were the only atom of the projected sig. This can be a very useful for simplifying (e.g.) finite-trace instances, since much of the clutter will be eliminated. When a projection is active, the theming window will give the option to change which atom is being used.

Styles

Style attributes such as font and line thickness for each sig and field can be customized. For fields only, clicking the "display as attribute" checkbox will tell Sterling to stop visualizing the field as an edge in the graph, and display it as an annotation on nodes.

Clicking a sig or field name will expand the style selection box for that sig or field. Click the name again to collapse the box.

Visualizing in Temporal Forge

In temporal mode, when the trace found is of length greater than 1, Sterling will enable a few new features:

• You can advance back and forth through the trace by using the arrow buttons in the Time drawer. Next to these buttons, Sterling will say which state the lasso loops back to. For instance, "Loop: 1" would mean that the lasso loops back to the second state (states are 0-indexed).
• Rather than one "Next" button, you'll see two: one labeled "Next" and the other "Next Config".
  • The "Next Config" button will ask the solver for a new trace that varies the non-variable relations of your model. If all your relations are variable, or if other constraints prevent a different non-variable subset of the instance from satisfying your run, this button will lead to a no-more-instances screen.
  • The "Next" button will ask the solver for a new trace that holds the non-variable relations constant. If there are no other traces possible without changing the non-variable relations, this button will lead to a no-more-instances screen.

The Evaluator

The evaluator provides a prompt that lets you query instances with Forge expressions. You can open the evaluator by clicking the "Evaluator" drawer on the far right of the Sterling window. Type a Forge expression and the evaluator will return its value in the current instance (assuming that Forge is still running). E.g.:

Because the evaluator works with respect to a single instance, exact values of expressions are returned. These expressions are (as of January 2024) not always Forge syntax. E.g., relations are displayed using nested parentheses, and false is written as #f. Fields are displayed in row form, with every entry in the field grouped into a parenthesis; in the example above, the meaning is that there's only one move on the board: X moved at row A, column C.

The Evaluator in Temporal Forge

If running in temporal mode, the evaluator is run in the context of the first state of the trace shown. To ask about later traces, use the ' or next_state operators. Remember that next_state applies to formulas, and ' applies to relational expressions. So in a directed graph you could ask whether there are edges in the second state via some edges' or after some edges.

Custom Visualizations: Script View

Sterling also allows you to write and run scripts that produce your own custom visualizations. This documentation site contains a basic example here:

• example visualization script
• Tic-tac-toe model to run the script with

If you want to try out this example, do the following:

Step 1: Open the Forge model and run it (racket ttt.frg). Sterling should open in your web browser, defaulting to the directed-graph visualization---which isn't very useful for this model. You should see something like this:

Step 2: Click the Script button on the upper-right of the window. This will switch to custom script view mode. Paste the script into the editor, then click the Run button. You should see something like this before clicking Run:

After running, you should see something like this, with a sequence of board states displayed on the left-hand side of the screen:

More Information

For more complex examples, library documentation, instructions on writing your own visualizers, etc. see Custom Visualizations.

Bounds

Forge is a bounded model finder, meaning it can only look for instances up to a certain bound. You can specify bounds in two seperate ways in Forge: using numeric bounds or instance bounds.

Numeric bounds (also called "scopes")

The most basic way of specifying bounds in Forge is providing a maximum number of objects for each sig. If no bound is specified, Forge defaults to allowing up to 4 of each sig. The default bound on Int is a bitwidth of 4 (16 integers total).

Numeric bounds can be provided explicitly per sig in a run, assert, etc. command by adding a trailing for ... after the constraint block (see Running).

run { ... } for 5 Cat
run { ... } for 5 Cat, 2 Dog

Note that this sets an upper bound on the size of instances Forge will show you. In other words, Forge will search for instances of size up to the bound you specify. If you instead want to set an exact bound, you can add the exactly keyword per sig. You may mix and match exact and upper numeric bounds as desired.

run { ... } for exactly 5 Cat
run { ... } for exactly 5 Cat, 2 Dog

Instance bounds

Instance bounds allow you to encode specific partial instances that you want Forge to run on. When creating an instance bound, you give upper and lower bounds in terms of concrete objects, not numeric sizes. This allows you to test your predicates on a specific instance, which can be convenient (see Examples). It is also useful for optimization in some cases (see Partial Instances, which use the same bounds syntax as examples).

sig Person {
    spouse: lone Person
}

inst exampleInstance {
    Person = `Person0 + `Person1 + `Person2
    spouse = `Person0 -> `Person1 + `Person1 + `Person0
}

example myExample is {marriageRules} for {
    Person = `Person0 + `Person1 + `Person2
    spouse = `Person0 -> `Person1 + `Person1 + `Person0
}

Note that Forge expects concrete object names to be prefixed with a backquote; this is mandatory, and used to distinguish object names (which only make sense in the context of an instance or instances) from sigs, fields, predicates, and other kinds of identifiers that make sense in arbitrary formulas.

Instances defined via inst can be used in run, assert, etc. and may be combined with numeric bounds, provided they are consistent. Bounds annotations, such as is linear, can be included in instance bounds as well. See the Concrete Instances section for more information about writing instance bounds.

run {} for 3 Int for {
    Person = `Person0 + `Person1 + `Person2
    spouse = `Person0 -> `Person1 + `Person1 + `Person0
}

run {} for 3 Int for exampleInstance

Concrete Instance Bounds

The types of problems that Forge creates and solves consist of 3 mathematical objects:

• A set of signatures and relations (the language of the problem);
• A set of logical/relational formulas (the constraints of the problem);
• A set of bounds on sigs and relations (the bounds of the problem).

Partial Instances

Forge presents a syntax that helps users keep these concerns separated. The first two concerns are represented by sig and pred declarations. The third concern is often addressed by numeric bounds (also called "scope"), but numeric bounds are always converted (usually invisibly to the user!) into set-based bounds that concretely specify:

• the lower bounds, what must be in an instance; and
• the upper bounds, what may be in an instance.

The inst syntax provides the ability to manipulate these set-based bounds directly, instead of indirectly via numeric bounds. The same syntax is used in example tests. Because bounds declarations interface more directly with the solver than constraints, at times they can yield performance improvements.

Finally, because bounds declarations can concretely refer to atoms in the world, we will often refer to them as partial instances.

inst Syntax

An inst declaration contains a {}-enclosed sequence of bind declarations. A bind declaration is one of the following, where A is either a sig name or field name.

• #Int = k: use bitwidth k (where k is an integer greater than zero);
• A in <bounds-expr>: specify upper bounds on a sig or field A;
• A ni <bounds-expr>: specify lower bounds on a sig or field A;
• A = <bounds-expr>: exactly specify the contents of the sig or field A (effectively setting both the lower and upper bounds to be the same);
• no A: specify that A is empty;
• r is linear : use bounds-based symmetry breaking to make sure field r is a linear ordering on its types (useful for optimizing model-checking queries in Forge); and
• r is plinear : similar to r is linear, but possibly not involving the entire contents of the sig. I.e., a total linear order on A'->A' for some subset A' of A.

When binding fields, the binding can also be given piecewise per atom. Keep in mind that atom names should be prefixed by a backquote:

• AtomName.f in <bounds-expr> (upper bound, restricted to AtomName);
• AtomName.f ni <bounds-expr> (lower bound, restricted to AtomName);
• AtomName.f = <bounds-expr> (exact bound, restricted to AtomName); and
• no AtomName.f (exact bound contains nothing, restricted to AtomName). Piecewise bindings add no restrictions to other atoms, only those mentioned. They can improve readability if you're defining a field for many different atoms. There is an example below.

The specifics of <bounds-expr> depend on which Forge language you are using.

Froglet Style Bind Expressions

In Froglet:

• a <bounds-expr> for a sig is a +-separated list of atom names (each prefixed by backquote), sig names that have already been bounded, and integers (without backquotes).
• a <bounds-expr> for a field is a +-separated list of entries in that field, using atom names (each prefixed by a backquote), sig names that have already been bounded, and integers (without backquotes). Entries are defined using the (arg1, arg2, ...) -> result syntax, and may be either complete or piecewise.
  • a complete bind for a field

sig Person {
    gradeIn: pfunc Course -> Grade
}
sig Course {}
abstract sig Grade {}

Person = `Person0 + `Person1 + `Person2
Course = `Course0 + `Course1 + `Course2
Grade = `A + `B + `C 

gradeIn = (`Person0, `Course0) -> `A + 
          (`Person0, `Course1) -> `B + 
          (`Person1, `Course2) -> `C

`Person0.gradeIn = `Course0 -> `A + 
                   `Course1 -> `B
`Person1.gradeIn = `Course2 -> `C
no `Person2.gradeIn

This style of bind expression is still allowed in Relational Forge, so if you prefer it, feel free to continue using it!

Relational-Forge Style Bind Expressions

From the relational perspective, a <bounds-expr> is a union (+) of products (->) of object names (each prefixed by backquote), sig names, and integers. Bounds expressions must be of appropriate arity for the sig or field name they are bounding.

A = `Alice+`Alex+`Adam
f = `Alice->`Alex + 
    `Adam->`Alex
g in `Alice->2 

edges in Node

sig Node { edges: set Node }

Student = `Student0 + `Student1

Student = `Student0 + `Student1
Person = Student + `Teacher0

inst in Temporal Forge

Temporal Forge also supports inst using the same syntax above.

Notes on Semantics

Bounds declarations are resolved in order before the problem is sent to the solver. The right-hand side of each declaration is evaluated given all preceding bounds declarations, which means that using sig names on the right-hand side is allowed so long as those sigs are exact bounded by some preceding bounds declaration.

A bounds declaration cannot define bounds for a sig unless bounds for its ancestors are also defined. Bounds inconsistencies will produce an error message.

Mixing Numeric Scope and inst

You can mix both styles; just give the set-based bounds after the numeric ones.

run {myPred} for 5 Person for {Class = `Class0 + `Class1}

However, beware of inconsistencies! Numeric and inst bounds are (as of January 2024) only reconciled right before the solver is invoked, so you might receive confusing error messages of "last resort" in case of inconsistency between the two.

Options

Forge has a number of options that affect how it functions and how its solver is configured. They all have the same form: option <key> <value>. Settings are case sensitive. The available setting keys are:

• verbose: governs the amount of information provided in the REPL. 1 is standard; 0 will omit statistical information (useful for test suites); 10 will print exceedingly verbose debugging information. Values between 1 and 10 gradually increase verbosity.
• solver: sets the solver used by Forge's worker process. The default is SAT4J, a Java-based solver. Other solvers can be more performant, and produce different instance orderings, depending on model. The MiniSatProver solver will enable extraction of unsat cores. Support for native solvers varies by OS. Currently:
  • MacOS (x64 and arm64 .dylib):
    • MiniSat, MiniSatProver, and Glucose
  • Linux (.so):
    • MiniSat, MiniSatProver, and Glucose
  • Windows (.dll):
    • MiniSatProver
  • All:
    • "<path-to-solver>", which lets you run a solver of your own that accepts DIMACS input (see the section below for instructions).
• logtranslation: controls how much of the translation from Forge to boolean logic is logged. The default is 0; must be 1 or higher to extract unsatisfiable cores.
• coregranularity: controls how fine-grained an unsatisfiable core will be returned. Default is 0. Suggested value is 1 if you want to see cores.
• core_minimization: controls whether cores are guaranteed minimal. Default is off. For minimal cores, use rce; hybrid is not guaranteed minimal but is often better than off while being faster than rce.
• sb: controls maximum size of symmetry-breaking predicate. 20 is default. Higher numbers increase Forge's ability to rule out equivalent instances, at a potential performance cost.
• skolem_depth: gives how many layers of universal quantifiers to Skolemize past. Default is 0; to disable Skolemization, give -1.
• engine_verbosity: sets the Logger level used by Pardinus (default=0). The following table is current as of version 1.5.0 (when the option was added):

case 0 : return Level.OFF;
case 1 : return Level.SEVERE;
case 2 : return Level.WARNING;
case 3 : return Level.INFO;
case 4 : return Level.FINE;
case 5 : return Level.FINER;
case 6 : return Level.FINEST;
default : return Level.ALL;

• run_sterling: decides whether to use the Sterling visualizer. Default is on. To disable, give off. Alternatively, pass a string containing the file path of a visualizer script to auto-load it in Sterling.
• sterling_port: sets the port used by the Racket web-server that Sterling connects to. The default picks an unused ephemeral port.
• test_keep: controls Forge's behavior when running test suites. The default (first) will cause Forge to stop immediately on the first test failure. The only currently-supported alternative (last) will cause Forge to run all tests and print a report at the end; only the final test failure will remain open for use with Sterling.
• problem_type: used to enable temporal_mode for Alloy6-style LTL support. This option is deprecated in favor of using #lang forge/temporal instead, and may be removed in future versions.
• no_overflow (default: false): when set to true, enables the Pardinus/Kodkod backend's overflow protection. This will exclude instances which satisfy the given problem only due to bitwidth overflow semantics. E.g., Counter.x = add[2,2] would not be satisfiable at bitwidth 3 with this option set to true, because 4 is greater than the maximum value available with 3 bits.

sig Node {edges: set Node}
run {}
option verbose 10
run {}
option verbose 1
run {}

Custom Solvers

Forge can use a solver of your choice to produce instances; this is most often used to experiment with the solver you build in the DPLL homework. There are a few factors to be aware of.

Limitations

While the "Next" button will be enabled in Sterling, the custom solver functionlity will always return the first instance found by the custom solver. There is also no support for unsatisfiable-core extraction; the custom solver will only report "unsat" for an unsatisfiable problem.

Instructions

To invoke a custom solver, provide a double-quoted filepath literal as the solver name:

option solver "<filepath-to-solver>"

Note that:

• the file must exist at the path specified;
• the file must be executable;
• the file must implement the DIMACS input/output format given in the DPLL assignment stencil;
• if the file is a script using a #! preamble, the preamble must point to the correct location. E.g., if the file is a Python script that begins with #!/usr/bin/python3, your Python 3 executable must reside at /usr/bin/python3.

The solver engine doesn't return rich information in the case of failure. Should any of these conditions not be met, you'll see a generic Pardinus crash error.

Examples

If you want to create a batch script on MacOS or Linux, you might try something like this in a run.sh file:

#!/bin/sh
python3 solver.py $1

On windows, you could try something like this, in a run.bat file:

@ECHO OFF
python3 solver.py %1

You might then invoke your solver via a .frg file like this:

#lang forge

-- MacOS or Linux:
option solver "./run.sh"

-- Windows:
-- option solver "./run.bat"


sig Node {edges: set Node}

test expect {
    s: {some edges} for 1 Node is sat
    u: {no edges 
        all n: Node | some n.edges} for exactly 1 Node is unsat
        
}

-- This will work, but will only ever show one instance:
--run {}

If your script can be executed directly, then you can replace ./run.sh in the above with the path to your script, including filename. On Windows, you will only be able to reference .bat or .exe files in your Forge solver option.

Testing

Forge supports several different testing constructs:

• example, for expressing that specific instances should satisfy (or not satisfy) a predicate;
• assert, for expressing that a specific predicate should be necessary or sufficient for another; and
• test expect, an expressive and general form that can be somewhat more difficult to use.

If tests pass, they do not open the visualizer, making them well-suited for building test suites for your Forge models.

Note on terminology: we will sometimes refer to assert and (some) test expect tests as property tests. This is because they can be used to express sweeping expectations about predicates, rather than just the point-wise, single-instance expectations that example can.

abstract sig Player {}
one sig X, O extends Player {}
sig Board { board: pfunc (Int -> Int) -> Player }
pred wellformed {
  all b: Board | all row, col: Int | {
    (row < 0 or row > 2 or col < 0 or col > 2) implies
      no b.board[row][col] 
  } 
}

Examples

The example syntax lets you test whether a specific instance is satisfied by some predicate in your model. An example contains three parts:

• a name for the example;
• which predicate the instance should satisfy (or not satisfy); and
• the instance itself.

example diagonalPasses is {wellformed} for {
  Board = `Board0
  X = `X0 
  O = `O0
  A = `A0
  B = `B0
  C = `C0
  `Board0.board = (0,0)->`X + (1,1)->`X + (2,2)->`X
}

Examples are analogous to unit tests in Forge. Every example says that if the instance were passed to the predicate, the predicate would return true (or false). This means that examples are a great way to explore potential design choices and map out your intent when modeling.

How do examples work?

An example passes if and only if the instance given is consistent with the predicate given.

example exampleYes is {wellformed} for {
  Board = `Board0
  X = `X0 
  O = `O0
  A = `A0
  B = `B0
  C = `C0  
}
example exampleNo is {not wellformed} for {
  Board = `Board0
  X = `X0 
  O = `O0
  A = `A0
  B = `B0
  C = `C0  
}

Notes on Example Syntax

The block within the second pair of braces must always be a concrete instance. That is, a series of assignments for each sig and field to some set of tuples, defined over atom names. Atom names must be preceded by a backquote; this reinforces the idea that they are atoms in a specific instance, rather than names in the model. You will not be able to refer to these atoms in predicates and most other Forge syntax.

Don't try to assign to the same field twice. If you want a field to contain multiple entries, use + instead. Remember that = in the context of an instance is assignment, not a constraint, and that most constraints won't work inside an instance.

Names of sigs may be used on the right-hand-side of an assignment only if the block has previously defined the value of that `sig`` exactly, allowing straightforward substitution.

Assert

The assert syntax allows you to write tests in terms of necessary and sufficient properties for a predicate.

pred fullFirstRow {some b: Board | b.board[0][0] = X and b.board[0][1] = X and b.board[0][2] = X}
pred someMoveTaken {some b: Board, row, col: Int | some b.board[row][col] }

assert fullFirstRow is sufficient for winning for 1 Board
assert someMoveTaken is necessary for winning for 1 Board

Assertions also support universal quantification (i.e. all, but not some, one, lone, etc). For example, if you instead wrote the predicates:

pred fullFirstRow[b : Board] {b.board[0][0] = X and b.board[0][1] = X and b.board[0][2] = X}
pred someMoveTaken[b : Board, row : Int, col : Int] {some b.board[row][col] }

assert all b : Board | fullFirstRow[b] is sufficient for winning for 1 Board
assert all b : Board, row, col : Int | someMoveTaken[b, row, col] is necessary for winning for 1 Board

Assertions are an excellent way to check and document your goals and assumptions about your model. In a more complex setting, we might write assertions that enforce:

• Dijkstra's algorithm doesn't terminate until the destination vertex has been reached;
• for a game of chess to be won, a king must be in check; or
• someone must first be logged into Gmail to read their mail.

Notes on Assert Syntax

Both the left- and right-hand-side of the assertion must be predicate names. That is, you cannot provide arbitrary formulas enclosed in brackets to an assert. This restriction eases some analysis but also encourages you to create reusable predicates.

Test-Expect Blocks

Forge's test expect blocks are the most general, but also the most complex, form of testing in the tool. You don't need to provide a concrete, specific instance for test expect, and can check general properties.

Every test expect contains a set of individual checks. Each has:

• an optional test name;
• a predicate block; and
• an intention (is sat, is unsat, or is theorem).

The meaning of each intention is:

• is sat: the predicate block is satisfiable under the given bounds;
• is unsat: the predicate block is unsatisfiable under the given bounds; and
• is theorem: the predicate block's negation is unsatisfiable under the given bounds.

Like the other test forms, each test may be accompanied by numeric scopes and inst bounds.

test expect { possibleToMove: {someMoveTaken} is sat }  

Suites: Organizing Your Tests

You should organize your tests into test suites for each predicate you plan to test.

test suite for winning {
  assert fullFirstRow is sufficient for winning for 1 Board
  assert someMoveTaken is necessary for winning for 1 Board
  
  test expect { possibleToWin_withoutFullFirstRow: {winning and not fullFirstRow} is sat } 
  
  example diagonalWin is {winning} for {
    Board = `Board0
    X = `X0 
    O = `O0
    A = `A0
    B = `B0
    C = `C0
    `Board0.board = (0,0)->`X + (1,1)->`X + (2,2)->`X
  }
}   

Test suites can only contain tests of the above forms, and all tests should reference the predicate under test.

Integers

Forge supports bit-vector integers. That is, the Forge Int sig does not contain an infinite set of mathematical integers. Rather, an instance's Int sig contains a representation of a subset of the integers following two's-complement encoding for a specific number of bits. Concretely, if the bitwidth is $k$, the integers in an instance will be the interval $[-2^{k-1},2^{k-1}-1]$. The default bitwidth is 4.

Remark

There are technically two types of "integers" in Forge: integer values (e.g. 4) and integer atoms (e.g. the atom representing 4 in a given instance). You can think of this as roughly similar to the primitive-int vs. object-Integer distinction in Java, although the analogy is not perfect. Forge will usually be able to automatically convert between these two, and you shouldn't usually have to think about the difference. We still mention it here for completeness.

Integer Operators

In the following, <atoms> represents a set of integer atoms and <value>, <value-a> and <value-b> are integer values.

• add[<value-a>, <value-b> ...]: returns the value of the sum value-a + value-b + ...
• subtract[<value-a>, <value-a> ...]: returns the value of the difference value-a - value-b - ...
• multiply[<value-a>, <value-b> ...]: returns the value of the product value-a * value-b * ...
• divide[<value-a>, <value-b> ...]: returns the value of the left-associative integer quotient (value-a / value-b) / ...
• remainder[<value-a>, <value-b>]: returns the remainder for doing integer division. Note that if value-a is negative, the result will also be negative, and that integer wrap-around may affect the answer.
• abs[<value>]: returns the absolute value of value
• sign[<value>]: returns 1 if value is > 0, 0 if value is 0, and -1 if value is < 0

Comparison operators on values

You can compare integer values using the usual =, <, <=, >, and >=.

Counting

Given an arbitrary expression e, the expression #e evaluates to the cardinality of (i.e., number of elements in) e. In Froglet, this is nearly always either 0 or 1, although full Forge allows expressions that evaluate to sets of arbitrary size.

Counting in Froglet

It is often useful to count even in Froglet, where expressions usually evaluate to either none or some singleton object. For example, in a tic-tac-toe model we might want to count the number of X entries on the board. In both Froglet and Forge, we can write this using a combination of # and set comprehension (normally not available in Froglet): #{row, col: Int | b.board[row][col] = X}.

Concretely:

#{x1: T1, ..., xn: Tn | <fmla>}

evaluates to an integer value reflecting the number of tuples o1, ... on where <fmla> is satisfied when x1 takes the value o1, etc.

Aggregation and Conversion

To convert between sets of integer atoms and integer values there are the following operations:

• sing[<value>]: returns an integer atom representing the given value;
• sum[<atoms>]: returns an integer value: the sum of the values that are represented by each of the int atoms in the set;
• max[<atoms>]: returns an integer value: the maximum of all the values represented by the int atoms in the set; and
• min[<atoms>]: returns an integer value: the minimum of all the values represented by the int atoms in the set.

While you might use sum, max, and min, you shouldn't need to use sing---Forge automatically converts between integer values and integer objects. If you do find you need to use sing, notify us ASAP!

Sum Aggregator

You should be cautious using sum[...] once you start using the Relational Forge language. Suppose you have sig A { i: one Int }, and want to sum over all of the i values for every A. Duplicate values for i may exist across multiple A atoms. Then sum[A.i] would not count duplicates separately, since A.i evaluates to a set, which can have no duplicates!

Because of this problem, Forge provides a second way to use sum which does count duplicates:

sum <x>: <set> | { <int-expr> }

Above, x is a variable name, set is the set you are quantifying over (currently only arity-1 sets are supported), and int-expr is an expression that evaluates to an integer value. The result of this entire expression is also an integer value. This counts duplicate integer values provided the atoms (of any type) in "relation" are different. The following example illustrates the difference between the two different uses of sum.

inst duplicates {
    A = `A0 + `A1
    time = `A0 -> 1 + `A1 -> 1
}

The Successor Relation

Forge also provides a successor relation, succ (Int -> Int) where each Int atom points to its successor (e.g. the Int atom 4 points to 5). The maximum Int atom does not point to anything.

Constants & Keywords

Constants

Forge provides a few built-in constants:

• univ (arity 1): the set of all objects in the universe (including Ints);
• none (arity 1): the empty set (to produce higher-arity empty relations, use the -> operator. E.g., a 2-ary empty relation would be represented as none -> none );
• iden: the identity relation (a total function from all objects in the universe to themselves, including Ints);
• Int: the set of available integer objects. By default it contains -8 to 7 inclusive, since the default bitwidth is 4. See Integers for more information.

Keywords

The following is a list of keywords in Forge that may not be used as names for relations, sigs, predicates, and runs. These include:

• state, transition (reserved for future use)
• sig, pred, fun
• test, expect, assert, run, check, is, for
• names of arithmetic operators, helpers, and built-in constants (e.g., add, univ, and reachable)

Helpers

Forge and Frglet provide a number of built-in helpers to ease your work in the language.

Sequences

A sequence is a field f of the form f: pfunc Int -> A (where A can be any sig) such that:

• f is a partial function (i.e., each Int has at most one corresponding entry);
• no index Int is less than zero; and
• indexes are contiguous (e.g., if there are entries at index 1 and index 3, there must be one at index 2).

You can think of sequences as roughly analogous to fixed-size arrays in a language like Java. To tell Forge that a partial-function field f is a sequence, use the isSeqOf predicate.

Hint: make sure that you use isSeqOf in any test or run that you want to enforce that f is a sequence. The isSeqOf predicate is just another constraint: it's not a persistent declaration like pfunc is.

isSeqOf

• isSeqOf[f, A]: a predicate that holds if and only if f is a sequence of values in A.

Sequence Helpers

The following helpers are also available, but should only be used when f is a sequence:

Sequence Helper Functions:

• seqFirst[f]: returns the first element of f, i.e. f[0].
• seqLast[f]: returns the last element of f.
• indsOf[f, e]: returns all the indices of e in f.
• idxOf[f, e]: returns the first index of e in f.
• lastIdxOf[f, e]: returns the last index of e in f.
• elems[f]: returns all the elements of f.
• inds[f]: returns all the indices of f.

Sequence Helper Predicates:

• isEmpty[f]: true if and only if sequence f is empty.
• hasDups[f]: true if and only if sequence f has duplicates (i.e., there are at least two indices that point to the same value).

Reachability

Forge provides a convenient way to speak of an object being reachable via fields of other objects.

• reachable[a, b, f]: object a is reachable from b through recursively applying field f. This predicate only works if a.f is well-defined.
• reachable[a, b, f1, f2, ...]: an extended version of reachable which supports using more than one field to reach a from b.

The extended version of reachable is useful if you wish to model, e.g., binary trees where nodes have a left and right field. In such a model, if you want to quantify over all descendents of a parent node, you might write all n: Node | reachable[n, parent, left, right].

Temporal Forge Overview

Temporal mode extends Forge with temporal operators to ease specification and checking of dynamic systems. This mode draws heavily on the Electrum work by INESC TEC and ONERA, and the newer Alloy 6 version, but there are (slight) differences.

To use Temporal Forge, just use #lang forge/temporal. This will cause a number of changes in how Forge processes your models, the largest one being that it will now always search for lasso traces (see below) rather than arbitrary instances. The maximum length of the trace is given by option max_tracelength <k> and defaults to 5. The minimum length of the trace is given by option min_tracelength <k> and defaults to 1.

Variable state (var)

Electrum mode allows var annotations to be placed on sig and field definitions. Such an annotation indicates that the contents of the corresponding relation may vary over time. Any sigs or fields that are not declared var will not vary over time.

Temporal Mode Semantics (Informally)

When the temporal solver is enabled, instances are always traces, and a trace is an infinite object, containing a state for every natural number $k$. However, the solver underlying Forge needs to finitize the problem in order to solve it. The solution to this, given a finite state-space, is to invoke the Pigeonhole Principle and seek traces that end in a loop: "lassos".

Temporal formulas and expressions are always evaluated with respect to a state index. At the top level of any formula, the index is $0$ (the first state of the trace). Temporal operators either change or "fan out" across multiple state indexes to let you express things like:

• "in the next state, ..." (add 1 to the state index)
• at some point in the future, ... (search for some state index)
• at all points in the future, ... (check all future indexes)
• ...

Added relational operators: priming

Electrum mode adds one relational operator: priming ('). Any relational expression that is primed implicitly means "this expression in the next state". Thus, you can use priming to concisely write transition effects.

Added formula operators

Electrum mode adds a number of formula operators, corresponding to those present in Linear Temporal Logic (LTL) and Past-Time Linear Temporal Logic.

Traditional LTL (future time)

Next State

• next_state <fmla> is true in a state i if and only if: fmla holds in state i+1.

let oldCount = Counter.count | 
    next_state Counter.count = add[oldCount, 1]

next_state Counter.count = add[Counter.count, 1]

Always (now and in the future)

• always <fmla> is true in a state i if and only if: fmla holds in every state >=i.

Eventually (now or sometime in the future)

• eventually <fmla> is true in a state i if and only if: fmla holds in some state >=i.

Until and Release (obligations)

• <fmla-a> until <fmla-b> is true in a state i if and only if: fmla-b holds in some state j>=i and fmla-a holds in all states k where i <= k < j. Note that the obligation to see fmla-a ceases in the state where fmla-b holds.

A natural question to ask is: what happens if fmla-b holds at multiple points in the future? However, this turns out not to matter: the definition says that the until formula is true in the current state if fmla-b holds at some point in the future (and fmla-a holds until then).

There is an alternative way to express obligations, which we won't use much:

• <fmla-a> releases <fmla-b> is true in a state i if and only if: fmla-a holds in some state j>=i and fmla-b holds in all states k where i <= k <= j, or fmla-a never occurs in a later state and fmla-b holds forever after. Note that the intuitive role of the two formulas is reversed between until and releases, and that, unlike until, the obligation extends to the state where fmla-a holds.

Past-time LTL

Past-time operators are useful for concisely expressing some constraints. They don't add more expressive power to the temporal language, but they do sometimes make it easier to avoid adding state, etc.

Previous State

• prev_state <fmla> is true in a state i if and only if: fmla holds in state i-1.

Historically (always in the past)

• historically <fmla> is true in a state i if and only if: fmla holds in every state <=i.

Once (at some point in the past)

• once <fmla> is true in a state i if and only if: fmla holds in some state <=i.

Note for Alloy Users

Alloy 6 and Electrum use the keywords after and before where Forge uses next_state and prev_state. We changed Forge to use these (admittedly more verbose) keywords in the hopes they are more clear. For example, after sounds like it could be a binary operator; in English, we might say "turn left after 3 stops". Also, next_state is definitely a formula about the following state whereas after does not communicate the same sense of immediacy.

Custom Visualization Basics

As seen in the Sterling Visualizer section, Forge uses an adapted version of the Sterling visualization tool. One of the advantages of using Sterling is that users can create their own custom visualization scripts.

Script View and Modes

When viewing an instance in Sterling, there are three options for viewing an instance: Graph, Table, and Script. To swap to script-view mode, click on Script. Most of the screen will be taken up by 3 new panes:

• the visualization canvas (blank by default);
• the script editor; and
• a list of available variables that are available for scripts to use.

Where the "Next" button was in the graph visualizer, there will now be 4 more buttons:

• Run executes the visualization script when clicked.
• <div>, <canvas> and <svg> swap between visualization modes. The default is <svg>. This documentation focuses on the <svg> mode, because that is where most of the library support is.

const stage = new Stage()
stage.add(new TextBox({
  text: 'Hello!', 
  coords: {x:100, y:100},
  color: 'black',
  fontSize: 16
}))
stage.render(svg, document)

Custom scripts are written in JavaScript. JavaScript constructs like looping, mapping over lists, etc. are all available for your use.

Working with an Instance

Sterling uses a number of JavaScript classes to represent an instance. The alloy-ts library documentation describes these in more detail, but you should be aware of the following:

The Instance

The instance variable provides access to the current instance. If temporal mode is active, instance will refer to the current state; to get the entire list of states, use instances instead (which is only available in temporal mode).

Accessing Sigs and Fields

You can use the .signature(name) method of an instance to obtain an object representing a sig in the instance. Likewise, .field(name) will yield an object representing a particular field.

const stage = new Stage()
stage.add(new TextBox({
  text: `${instance.signature('IntArray')}`, 
  coords: {x:100, y:100},
  color: 'black',
  fontSize: 16
}))
stage.render(svg, document)

const stage = new Stage()
const theArray = instance.signature('IntArray').atoms()[0]
const elementsField = instance.field('elements')
stage.add(new TextBox({
  text: `${theArray.join(elementsField)}`, 
  coords: {x:100, y:100},
  color: 'black',
  fontSize: 16}))
stage.render(svg, document)

Built-in Library Shapes

Scripts in <svg> mode use the D3 visualization library by default. However, D3 can be fairly complex to use, and so various built-in helpers are also available. We encourage using the helper library, although in more advanced cases you may wish to use D3 directly.

Potential Pitfalls and Debugging

Sterling presents a "full Forge" view of instances, and one that's closer to the way the solver works. All sigs and fields are represented as sets in the instance. Each set contains AlloyTuple objects, which themselves contain lists of AlloyAtoms. Because (at the moment) there is no support for types in the script editor, it can sometimes be troublesome to remember which kind of datum you're working with. The alloy-ts docs below provide much more detail, but in brief:

• if the object has an .atoms() method, it's an AlloyTuple;
• if the object has an .id() method, it's an AlloyAtom; and
• signatures, fields, tuples, and atoms are all AlloySets and provide a .tuples() method.

In order to do a Froglet-style field access, you should use the .join method. (E.g., in the example above, we wrote theArray.join(elementsField) rather than theArray.elementsField or theArray.elements.)

We suggest using TextBoxes to visualize debugging information. As a fallback, you can also use console.log(...) as normally in JavaScript, but the web-developer console in Sterling can be somewhat congested. Printing raw AlloySet objects via console.log will also not be immediately useful, since Sterling uses a proxy to manage the difference between the set as Forge syntax and the set as a value in the instance.

Further Resources and Examples

Further chapters:

• Visualization Helper Library describes helpers (e.g., text boxes, grids, etc.) for visualization that don't require D3 knowledge.
• Working with SVG and Imports explains how to (e.g.) increase the size of the rendering area.

External resources:

• What is the SVG format?
• D3FX helpers design documentation---beware, this is actively being worked on and edited, and thus subject to change!

Examples using D3:

• Mia Santomauro's 2021 Guide for custom visualization in Forge is still useful, but was made before most of the helper functions and classes above existed. If you're interested in using D3 directly with Sterling, it's a great starting point.
• Tim's 2022 visualizer script examples also use D3 directly, rather than leveraging helpers, but may also be a useful reference:
  • Sudoku Synthesizer
  • Queue
  • Lights Puzzle (temporal mode)
• Tim and Mia also wrote a "visualizer" that plays musical scales generated by a model Tim wrote to understand music a bit better.

D3FX Helpers

The D3FX helpers library was designed as an interface between Sterling users and the D3 visualization library in Javascript. D3 was originally the primary way that Forge users wrote custom visualizations. However, we have found that using D3 in Sterling can involve a large amount of learning and prep time--especially for those without much experience with JavaScript.

D3FX was created to ease writing custom visualizations in Sterling. It contains a library of shapes and objects that were commonly used in the past, such as grid layouts and labeled arrows. Since custom visualizations are still written in JavaScript, using D3FX requires some knowledge of the language, but its object-oriented design is meant to ease basic use for those who might be familiar with languages like Java or Python.

This page contains documentation for all classes in D3FX, along with small examples of how to create and work with them. Complete, runnable examples can be found in the Forge repository's viz-examples directory.

new TextBox(`State:${idx}${lb}`,{x:0,y:0},'black',16)

new TextBox({text: `State:${idx}${lb}`, coords: {x:0,y:0}, color: 'black', fontSize: 16})

Further Resources

In addition to this page, you can view supplementary examples in the Forge repository here. Each contains both a Forge model to run (.frg) and the corresponding script file (.js).

The Stage and VisualObjects

Every element D3FX displays on the screen is represented by a VisualObject, which includes shapes like squares or circles, as well as more complicated objects like grids or trees.

To render visual objects, a Stage object needs to be created to contain them. After creating, the user can call stage.add(...) to place the visual object in the stage. To render all added VisualObjects, call stage.render(...). Below is some important information for interacting with these objects, specifically for those without JavaScript experience.

Props and Optional Parameters

All VisualObjects will take in a props (short for "properties") object. Props objects have a number of fields with designated types. These fields can be entered in any order with their corresponding names. For example:

new Rectangle({
    height: 100,
    width: 200,
    coords: {x: 100, y: 50},
    color: 'red',
    label: 'Hello'
})

For ease of use, we've written out a template for each of these props objects in terms of an interface, like the following:

interface Coords {
    x: number,
    y: number
}

Fields in such interface declarations may include a ?. This denotes that the field is optional.

Primitive Objects

A primitive object is one that doesn't visually contain any other D3FX objects.

TextBox

Text boxes render text to the screen at a given location. Their constructor accepts a props object of the following form:

interface TextBoxProps {
    text? : string,
    coords?: Coords,
    color?: string,
    fontSize?: number
}

Here is an example TextBox using these props:

let text = new TextBox({
    text: 'hello',
    coords: {x: 50, y:50},
    color: 'black',
    fontSize: 12
}) 

Additionally, TextBox supports script-defined callbacks. You can register events using the events prop. Supported events are described here.

new TextBox({
    text: 'hello',
    coords: {x: 50, y:50},
    color: 'black',
    fontSize: 12,
    events: [
        {event: 'click', callback: () => {console.log('clicked!')}}
    ]
}) 

ImageBox

An ImageBox contains an image loaded from a URL.

const stage = new Stage()
const box = new ImageBox({
    coords: {x:100,y:100}, 
    url: "https://csci1710.github.io/2024/static/media/LFS_FROG.8de0a0795d10898e5fe9.png", 
    width:200, 
    height:200})
stage.add(box)
stage.render(svg)

Primitive Shapes

The primitive object types Rectangle, Circle, and Polygon are all instances of a wider class called Shape. As a result, their props objects all implement the following interface:

interface ShapeProps {
  color?: string,
  borderWidth?: number,
  borderColor?: string,
  label?: string,
  labelColor?: string,
  labelSize?: number,
  opacity?: number
}

For ease of reading, these fields will be rewritten later on where applicable.

Rectangle

Rectangles take in a pair of coordinates corresponding to the top left corner of the shape, along with a width and height. The props object is of the following form:

interface RectangleProps extends shape {
    height: number,
    width: number,
    labelLocation?: string,
    coords?: Coords,

    // Borrowed from shape
    color?: string,
    borderWidth?: number,
    borderColor?: string,
    label?: string,
    labelColor?: string,
    labelSize?: number,
    opacity?: number
}

The value of label-location can be "center" (default). Other options include "topLeft", "topRight", "bottomLeft", and "bottomRight", which will generate text outside the rectangle in these locations.

Here is an example Rectangle using these props:

let rect = new Rectangle({
    coords: {x: 100, y:100},
    height: 20,
    width: 20,
    color: "pink",
    borderColor: "black",
    borderWidth: 2,
    label: "5"
})

Which renders the following:

Circle

Circles take in a pair of coordinates as the center and a radius, along with the rest of the following props object:

interface CircleProps extends ShapeProps {
    radius: number,

    // Borrowed from shape
    color?: string,
    borderWidth?: number,
    borderColor?: string,
    label?: string,
    labelColor?: string,
    labelSize?: number,
    opacity?: number
}

The text in the label will render in the center of the circle. Here is an example circle:

let circ = new Circle({
    radius: 10, 
    center: {x: 100, y:100}, 
    color: 'aqua', 
    borderWidth: 2, 
    borderColor: 'black', 
}); 

Which renders the following:

Polygon

Polygons are the most generic of the primitive shapes offered in D3FX. They take in any list of points and create a shape with those points on the perimeter. The props are of the form:

export interface PolygonProps extends ShapeProps {
    points: Coords[]

    // Borrowed from shape
    color?: string,
    borderWidth?: number,
    borderColor?: string,
    label?: string,
    labelColor?: string,
    labelSize?: number,
    opacity?: number
}

The label will be generated in roughly the center of the shape (the mean of the points entered). Here is an example of a polygon being used to create a (nonconvex) pentagon.

polypoints = [
    {x:100, y:200},
    {x:200, y:200},
    {x:175, y:150},
    {x:200, y:100},
    {x:100, y:100}
]

let poly = new Polygon({
    points: polypoints, 
    color: 'orange', 
    borderWidth: 2, 
    borderColor: 'black', 
    label: "Hi!",
    labelColor: "black" ,
    opacity: 0.7
});

Which will render the following pentagon:

Line

A Line takes in a series of points and creates a line passing through said points.

interface LineProps {
  points?: Coords[], 
  arrow?: boolean,
  color?: string, 
  width?: number,
  opacity?: number
  style?: string
}

If arrow is true, the end of the line will have a small arrowhead. Style can take the values of 'dotted' or 'dashed'Here's an example line:

polypoints = [
    {x:100, y:100},
    {x:125, y:100},
    {x:150, y:75},
    {x:200, y:125},
    {x:225, y:100},
    {x:250, y:100}
]

let line = new Line({
    points: polypoints, 
    color: 'black', 
    width: 2, 
    labelColor: "blue",
    arrow: true,
    style: "dotted"
});

Which will render:

Compound Objects

While the above objects are good for simple visualizations, managing the relationship between many primitive objects manually can be difficult. With this in mind, D3FX provides a number of compound objects, which automatically group their child objects in a particular way.

circ = new Circle({...})
comp = new SomeCompoundObject({innerObject: circ, ...}) // circ is a child object

stage.add(comp) // the stage will render comp, which then renders its child circ
stage.add(circ) // the stage will render circ (again)

Grid

Grids place visual objects into a 2-dimensional arrangement of cells. The grid constructor takes in the following props:

interface gridProps {
    grid_location: Coords, // Top left corner
    cell_size:{
        x_size:number,
        y_size:number
    },
    grid_dimensions:{
        x_size:number,
        y_size:number
    },
}

The grid_dimensions field should be a pair of positive integers, referring to the horizontal and vertical capacity of the array, respectively. The cell_size, in pixels, will be the size allocated for each of these objects in the rendered grid. Grids also offer the add method to fill these cells with VisualObjects:

add(
    coords: Coords, 
    add_object:VisualObject, 
    ignore_warning?:boolean
)

The coordinates should be integers designating which row and column of the grid to add the child object to. Notably, the child object's visual location will immediately be adjusted to fit the cell.

Adding a child object will produce an error if the child object does not fit into the given cell. To ignore this error, set the ignore_warning prop to true.

Here is an example of a simple grid:

let grid = new Grid({
    grid_location: {x: 50, y:50},
    cell_size: {x_size: 30, y_size: 30},
    grid_dimensions: {x_size: 4, y_size: 5}
})

grid.add({x: 0, y: 1}, new Circle({radius: 10, color: "red"}))
grid.add({x: 3, y: 3}, new Circle({radius: 10, color: "blue"}))

Here we have a 4x4 grid of 30x30 pixel squares, into two of which we place circles. Note that the circles added to the grid do not have coordinates. This is because the coordinates of these shapes are immediately changed to be in the center of the given squares in the grid. This renders as follows:

Tree

The Tree object renders a branching data structure. While in principle Sterling's default visualization can produce trees, the Tree object in D3FX allows a finer degree of control.

The nodes in a Tree object are themselves visual objects, which will then automatically be rendered with lines between them. The props for Tree are as follows:

interface TreeProps {
    root: VisTree, 
    height: number, 
    width: number, 
    coords?: Coords, 
    edgeColor?: string, 
    edgeWidth?: number
}

Where the VisTree interface logically represents a tree and its subtrees in recursive fashion:

interface VisTree{
    visualObject: VisualObject,
    children: VisTree[]
}

When rendered, the tree will be adjusted to exactly fit into the box with top-left corner designated by coords and dimensions designated by height and width. Here is an example tree with four layers:

let obj1 = new Circle({radius: 10, color: 'red', borderColor: "black", label: '1'});
let obj2 = new Circle({radius: 10, color: 'red', borderColor: "black", label: '2'});
let obj3 = new Rectangle({height: 20, width: 20, color: 'green', borderColor: "black", label: '3'});
let obj4 = new Circle({radius: 10, color: 'red', borderColor: "black", label: '4'});
let obj5 = new Circle({radius: 10, color: 'red', borderColor: "black", label: '5'});
let obj6 = new Circle({radius: 10, color: 'red', borderColor: "black", label: '6'});
let obj7 = new Circle({radius: 10, color: 'blue', borderColor: "black", label: '7'});
let obj8 = new Circle({radius: 10, color: 'blue', borderColor: "black", label: '8'});

let visTree = {
  visualObject: obj1,
  children: [
    {
      visualObject: obj2,
      children: [
        { visualObject: obj4, children: [] },
        {
          visualObject: obj5,
          children: [{ visualObject: obj8, children: [] }]
        },
        { visualObject: obj7, children: [] }
      ]
    },
    {
      visualObject: obj3,
      children: [{ visualObject: obj6, children: [] }]
    }
  ]
};

let tree = new Tree({
    root: visTree, 
    height: 200, 
    width: 200, 
    coords: { x: 100, y: 100 }
    });

which renders as:

Edge

Edges display relationships between objects, without requiring manual management of those objects' locations---unlike the primitive Line. Edge objects take in the following props:

export interface EdgeProps {
  obj1: VisualObject;
  obj2: VisualObject;
  lineProps: LineProps;
  textProps: TextBoxProps;
  textLocation: string;
}

Here, obj1 represents the first visual object, or the source of the edge, and obj2 is the sink. Styling, color, width, and more attributes of the edge itself can be designated in lineProps, which contains all the information that would normally be passed to a Line. Similarly, the label for the line is designated by textProps, which supports all relevant features used in the label's underlying TextBox object.

Lastly, textLocation allows for freedom in determining the location of the label. By default, the label will appear in the exact center of the line. However, passing in right, left, above, or below will offset the location by whatever orthogonal direction closest to the input. There is also support for clockwise or counterclockwise, which place the label in the stated location from the perspective of the source object. Here is an example of a few edges between visualObjects:

const rect = new Rectangle({width: 20, height: 20, coords: {x:200, y:50}})
const circ1 = new Circle({radius: 10, center: {x:150, y:200}})
const circ2 = new Circle({radius: 10, center: {x:250, y:200}})

const edge1 = new Edge({
    obj1: rect, obj2: circ1,
    textProps: {text: "e1", fontSize: 11},
    textLocation: "above"
})
const edge2 = new Edge({obj1: circ1, obj2: rect,
    textProps: {text: "e2", fontSize: 11},
    textLocation: "below"})
const edge3 = new Edge({obj1: circ1, obj2: circ2,
    textProps: {text: "e3", fontSize: 11},
    lineProps: {color: "green"},
    textLocation: "above"})
const edge4 = new Edge({obj1: rect, obj2: circ2,
    lineProps: {arrow: true},
    textProps: {text: "e4", fontSize: 11},
    textLocation: "above"})

// Adding all objects and circles to the stage individually before rendering. 

This renders as:

Working with SVG

Expanding the SVG Region

If the default svg area is not the right size for your needs, you can change its dimensions.

The <svg> element that scripts render to is contained within an element called svg-container, whose only child is the render area. Thus, the render area can be obtained with:

const renderArea = document.getElementById('svg-container').getElementsByTagName('svg')[0]

You can then set the style.width and style.height attributes of the rendering area.

const svgContainer = document.getElementById('svg-container')
svgContainer.getElementsByTagName('svg')[0].style.height = '500%'
svgContainer.getElementsByTagName('svg')[0].style.width = '100%'

Alternative Method

You also have access to set the viewBox attribute of the <svg> region. However, we don't suggest making this specific kind of low-level change if you're working only with D3FX.

require('d3')
d3.select(svg).attr("viewBox", "0 0 1000 1000")

Importing modules

Sterling uses the d3-require and jsdelivr systems to import external libraries. These should be given in the first lines of the script (before any comments!) and be enclosed in a single require form per library. E.g., to import the d3-array and d3-format libraries:

require("d3-array")
require("d3-format")

Attribute-Based Access Control

The Attribute-Based Access Control (ABAC) language can be enabled via #lang forge/domains/abac on the first line of a file. The syntax of the language is totally distinct from Froglet, Relational Forge, and Temporal forge.

Purpose

ABAC policies describe whether requests should be permitted or denied. Requests comprise three variables:

• s: the subject (i.e., the individual or program making the request);
• a: the action (i.e., the type of access being requested); and
• r: the resource (i.e., the file or other object being acted upon by the request).

policy original
  // Administrators can read and write anything
  permit if: s is admin, a is read.
  permit if: s is admin, a is write.
  // Files being audited can't be changed by customers
  deny   if: a is write, r is file, r is under-audit.
  // Customers have full access to files they own
  permit if: s is customer, a is read, s is owner-of r.
  permit if: s is customer, a is write, s is owner-of r.
end;

Policy Syntax

A policy declaration comprises a name and a set of a rules. The form is:

policy <NAME>
  <RULE1>
  <RULE2>
  ...
end;

Rule Syntax

A rule contains a decision and a sequence of conditions, terminated by a period.

<DECISION> if: <CONDITION1>, <CONDITION2>, ... .

Decisions may be either:

• permit; or
• deny.

Condition Syntax

Finally, a condition expresses a requirement involving one of the three request variables. If the condition involves only one variable, it takes the form <var> is <attribute>. If the condition involves two variables, it takes the form <var 2> is <attribute> <var 2>.

For the moment, the ABAC language is built for a specific assignment. Thus, the vocabulary of the language is restricted to the following attributes:

• for subjects: admin, accountant, and customer;
• for actions: read and write;
• for resources: file.
• for combinations of subject and resource: owner-of and under-audit.

Analysis Commands

For the purposes of this assignment, only one command should be necessary:

Comparing Policies

The compare command uses Forge to run a "semantic diff" on two policies. It will produce a single scenario that describes a request where the two policies differ in their decisions, along with which rule applied to cause the difference.

Like policies, commands must be terminated with a semicolon.

compare original modified;

Comparing policies original and modified...

-----------------------------------
Found example request involving...
a subject <s> that is:  Accountant, Employee
an action <a> that is:  Read
a resource <r> that is: File
Also,
  <r> is Audit

This rule applied in the second policy:
    permit if: s is accountant, a is read, r is under-audit.
Decisions: modified permitted; original denied

Other Commands

• info prints the names of policies currently defined.
• query can query the behavior of a single policy given a condition.

query original yields permit where s is not admin;

Implementation Notes

At the moment, there is no way to get another example from compare or query; in practice it would be implemented the same way that Forge's "next" button is.

Glossary

This glossary is meant to cover terms that aren't easily searched for via the search bar. E.g., it lists "arity" but not specific Forge language constructs like pred or sig.

Terms

The arity of a relation is the number of columns in the relation; that is, the number of elements of a tuple in that relation.

An atom is a distinct object within an instance.

An instance is a concrete scenario that abides by the rules of a model, containing specific atoms and their relationships to each other.

A model is a representation of a system. In Forge, a model comprises a set of sig and field definitions, along with constraints.

Glossary of Errors

This section contains tips related to some error terminology in Forge.

Errors Related to Bounds

Please specify an upper bound for ancestors of ...

If A is a sig, and you get an error that says "Please specify an upper bound for ancestors of A", this means that, while you've defined the contents of A, Forge cannot infer corresponding contents for the parent sig of A and needs you to provide a binding.

sig Course {}
sig Intro, Intermediate, UpperLevel extends Course {} 

example someIntro is {wellformed} for {
    Intro = `CSCI0150
}

example someIntro is {wellformed} for {
    Intro = `CSCI0150
    Course = `CSCI0150
}

Errors Related to Testing

Invalid example ... the instance specified is impossible ...

If an example fails, Forge will attempt to disambiguate between:

• it actually fails the predicate under test; and
• it fails because it violates the type declarations for sigs and fields.

Consider this example:

#lang forge/bsl 

abstract sig Grade {} 
one sig A, B, C, None extends Grade {} 
sig Course {} 
sig Person { 
    grades: func Course -> Grade,
    spouse: lone Person 
}

pred wellformed { 
    all p: Person | p != p.spouse 
    all p1,p2: Person | p1 = p2.spouse implies p2 = p1.spouse
}

example selfloopNotWellformed is {wellformed} for {
    Person = `Tim + `Nim 
    Course = `CSCI1710 + `CSCI0320
    A = `A   B = `B   C = `C   None = `None 
    Grade = A + B + C + None

    -- this violates wellformed
    `Tim.spouse = `Tim 
    
    -- but this violates the definition: "grades" is a total function
    -- from courses to grades; there's no entry for `CSCI0320.
    `Tim.grades = (`CSCI1710) -> B
    
}

If you receive this message, it means your example does something like the above, where some type declaration unrelated to the predicate under test is being violated.

Errors related to syntax

Unexpected type or Contract Violation

In Forge there are 2 kinds of constraint syntax for use in predicates:

• formulas, which evaluate to true or false; and
• expressions, which evaluate to values like specific atoms.

If you write something like this:

#lang forge/bsl 
sig Person {spouse: lone Person}
run { some p: Person | p.spouse}

some: contract violation
  expected: formula?
  given: (join p (Relation spouse))

The syntax is invalid: the some quantifier expects a formula after its such-that bar, but p.spouse is an expression. Something like some p.spouse is OK. (The phrase "contract violation" in this case just means "I was passed something I didn't expect.")

Likewise:

sig Person {spouse: lone Person}
run { all p1,p2: Person | p1.spouse = p2.spouse implies p2.spouse}

=>: argument to => had unexpected type. 
  expected #<procedure:node/formula?>,
  got (join p2 (Relation spouse))

Since implies is a boolean operator, it takes a formula as its argument. Unfortunately, p2.spouse is an expression, not a formula. To fix this, express what you really meant was implied.