add: ltlf model draft example

forge/examples/README.md

@@ -21,8 +21,12 @@ While many of these examples are commented heavily, the [Forge documentation](ht
 * `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. 
+* `examples/ltlf` contains a model of finite-trace linear temporal logic. 
+* `examples/network` contains a basic model of network forwarding. 
 
-For a more advanced example, see: 
+
+
+For more advanced examples, see: 
 
 * `examples/prim`, which contains a model of Prim's MST algorithm, with notes on verification.
 

forge/examples/ltlf/README.md

@@ -0,0 +1,6 @@
+# Finite-Trace LTL
+
+This is a basic model of finite-trace LTL. I (Tim Nelson) decided to build it while we were writing our [paper on LTLf misconceptions](https://cs.brown.edu/~tbn/publications/ltlf-misconceptions.pdf). I didn't finish it at the time, but wrapped it up in early 2025. 
+
+I'm including it in Forge's standard example suite as a counterpoint to the boolean logic model: both represent the syntax and semantics of a logic, but LTLf adds the complication of traces and time indexes, and so involves a few different modeling choices. 
+

forge/examples/ltlf/ltl_f.frg

@@ -0,0 +1,162 @@
+#lang forge
+/*
+  Modeling finite-trace LTL in Forge
+  TN January 2023
+
+  LTLf is similar to standard LTL, except that it is interpreted over finite traces. 
+  In some ways, this makes it similar to the finite-trace idiom we used to model 
+  executions before moving to Relational Forge, but there are key differences. 
+  As a result, it might be especially useful to model it and make sure we understand 
+  it! (Please remember: this is a different logic than what Temporal Forge uses.)
+
+  I'm modeling this a bit differently from the boolean-logic model to show a few 
+  techniques that might be useful. 
+  
+  We want to represent multiple traces in the same instance. So we need to 
+  separate "state" from "state index", either by using Int or by making 
+  a new Index type that must be ordered. I decided to use Ints, and to avoid 
+  needing an optimizer instance I'm just declaring traces to start at min[Int].
+*/
+
+/** Disable integer overflow, since we use ints as state indexes */
+option no_overflow true
+
+-------------------------------------------------------
+-- Formulas of LTLf 
+--   leaving out R(elease) and X_w, since they can be desugared
+--   via X, Not, and U. Similarly, leaving out implies and iff.
+-------------------------------------------------------
+
+/** Enum tags for operators */
+abstract sig UOP, BOP {}
+one sig Not, Next, Eventually, Always extends UOP {}
+one sig And, Or, Until extends BOP {}
+
+/** Formulas are either atomic propositions, unary operator applications, or binary 
+    operator applications. */
+abstract sig Formula {}
+/** We called this "Var" in the boolean-logic model. */
+sig Var extends Formula {}
+sig Unary extends Formula {
+    uop: one UOP,
+    sub: one Formula
+}
+sig Binary extends Formula {
+    bop: one BOP,
+    left: one Formula,
+    right: one Formula
+}
+
+/** Notice how using enum tags simplifies this helper function. */
+fun subformulas[fmla: Formula]: set Formula {
+    fmla.^(sub + left + right)
+}
+pred wellformed_formulas {
+    all f: Formula | f not in subformulas[f]
+}
+
+-------------------------------------------------------
+-- Semantics: Finite traces
+-------------------------------------------------------
+
+/** Finite, possibly empty sequences of states. In contrast to the 
+    boolean-logic model, we're using integers as time-indexes. But since 
+    these traces are finite, we need to keep track of the ending index. 
+    
+    Ideally, we'd declare traces start at idx=0, and use an optimizer instance 
+    to deal with this. 
+    */
+sig Trace {    
+    /** The last populated index of the trace. We assume traces are not empty. */
+    endIdx: one Int,
+    /** The atomic truths at each state: which variables are set to true? */
+    truths: set Int -> Var
+}
+
+/** Helper that returns the set of integer indexes that are valid for this trace. */
+fun states[t: Trace]: set Int {
+    -- every pre-state and every post-state in the trace
+    {i: Int | i <= t.endIdx}
+}
+
+/** Helper that returns the set of integer indexes that are both valid and >= s. */
+fun laterOrNow[t: Trace, s: Int]: set Int {
+    {i: Int | i <= t.endIdx and i >= s}
+}
+
+pred wellformed_traces {
+    -- There are no truths outside the valid indexes for this trace. 
+    all t: Trace | t.truths.Var in states[t]
+    -- There are no lifted truths outside the valid indexes for this trace.
+    all t: Trace | (Semantics.table[t]).Var in states[t]
+}
+
+one sig Semantics {
+    /** This could be a field of Trace as well, but I pulled it out while I was 
+    working on fixing an issue and kept it this way. This is a "lifting" of the 
+    `truths` relation to arbitrary formulas.  */
+    table: set Trace -> Int -> Formula
+}
+
+/** Same trick as in boolean logic. 
+    This trick won't always work, but it does for tree-shaped data.
+    
+    Using definitions from https://cs.brown.edu/~tbn/publications/ltlf-misconceptions.pdf
+*/
+pred semantics {
+    all t: Trace, s: Int, f: Formula | t->s->f in Semantics.table iff { 
+        s in states[t] and {
+        -- Var case: if the state at index <s> sets this variable to true
+        f in Var and f in t.truths[s]
+        or
+        -- Not case
+        f.uop = Not and {
+            t->s->(f.sub) not in Semantics.table           
+        }
+        or
+        -- Eventually case
+        f.uop = Eventually and {            
+            some s2 : laterOrNow[t, s] | t->s2->(f.sub) in Semantics.table            
+        }
+        or
+        -- Always case
+        f.uop = Always and {
+            all s2 : laterOrNow[t, s] | t->s2->(f.sub) in Semantics.table
+        }
+        or
+        -- Next case
+        f.uop = Next and {
+            t->add[s,1]->(f.sub) in Semantics.table
+        }
+        or
+        -- And case
+        f.bop = And and {
+            t->s->(f.left) in Semantics.table and
+            t->s->(f.right) in Semantics.table
+        }
+        or
+        -- Or case
+        f.bop = Or and {
+            t->s->(f.left) in Semantics.table or
+            t->s->(f.right) in Semantics.table
+        }
+        or
+        -- Until case (*easier* to express without lasso traces!)
+        f.bop = Until and {
+            some s2: laterOrNow[t, s] | {
+                t->s2->(f.right) in Semantics.table
+                -- Note that the LHS obligation doesn't hold in the moment the RHS becomes true. 
+                all smid: Int | (smid >= s and smid < s2) implies 
+                                  t->smid->(f.left) in Semantics.table
+
+            }
+        }
+    }}
+
+}
+
+exampleForVisualizing: run {
+    wellformed_formulas
+    wellformed_traces
+    semantics
+} for exactly 5 Formula, exactly 3 Var, exactly 2 Trace

forge/examples/ltlf/ltl_f.test.frg

@@ -0,0 +1,94 @@
+#lang forge
+
+open "ltl_f.frg"
+
+/*
+  Rough example-based tests of LTLf semantics.
+*/
+
+-- always { eventually { p or q }}
+one sig GFPORQ, FPORQ extends Unary {}
+one sig PORQ extends Binary {}
+one sig P, Q extends Var {}
+-- next_state { p }
+one sig XP extends Unary {}
+-- {p} until {q}
+one sig PUQ extends Binary {}
+-- not {p or q}
+one sig NPORQ extends Unary {}
+
+-- Traces
+one sig TraceA, TraceB, TraceC extends Trace {}
+
+pred wellformed_example_gfporq {
+    // Set up the formulas
+    GFPORQ.uop = Always
+    GFPORQ.sub = FPORQ
+    FPORQ.uop = Eventually
+    FPORQ.sub = PORQ
+    PORQ.bop = Or
+    PORQ.left = P
+    PORQ.right = Q
+    XP.uop = Next 
+    XP.sub = P
+    PUQ.bop = Until
+    PUQ.left = P
+    PUQ.right = Q
+    NPORQ.uop = Not 
+    NPORQ.sub = PORQ
+
+    // A: none -> p -> q -> pq  (-8, -7, -6, -5)
+    TraceA.endIdx = -5
+    TraceA.truths[-8] = none
+    TraceA.truths[-7] = P
+    TraceA.truths[-6] = Q 
+    TraceA.truths[-5] = P + Q
+
+    // B: p -> q -> pq (-8, -7, -6)
+    TraceB.endIdx = -6
+    TraceB.truths[-8] = P
+    TraceB.truths[-7] = Q
+    TraceB.truths[-6] = P + Q
+
+    // C: none -> p -> none -> q
+    TraceC.endIdx = -5
+    TraceC.truths[-8] = none
+    TraceC.truths[-7] = P
+    TraceC.truths[-6] = none
+    TraceC.truths[-5] = Q
+
+}
+
+test_gfporq_consistent: assert {
+    wellformed_formulas
+    wellformed_traces
+    semantics
+    wellformed_example_gfporq
+} is sat for exactly 8 Formula, exactly 3 Trace
+
+/* Note this will fail for higher bounds on Formula, 
+   since new fmlas might also be satisfied by the traces. */
+pred gfporq_semantics {
+    Semantics.table[TraceA][-8] = GFPORQ + FPORQ + XP + NPORQ
+    Semantics.table[TraceA][-7] = GFPORQ + FPORQ + PORQ + PUQ + P
+    Semantics.table[TraceA][-6] = GFPORQ + FPORQ + PORQ + XP + PUQ + Q
+    Semantics.table[TraceA][-5] = GFPORQ + FPORQ + PORQ + PUQ + P + Q
+
+    Semantics.table[TraceB][-8] = GFPORQ + FPORQ + PORQ + PUQ + P
+    Semantics.table[TraceB][-7] = GFPORQ + FPORQ + PORQ + XP + PUQ + Q
+    Semantics.table[TraceB][-6] = GFPORQ + FPORQ + PORQ + PUQ + P + Q
+
+    // C: none -> p -> none -> q
+    Semantics.table[TraceC][-8] = GFPORQ + FPORQ + XP + NPORQ
+    Semantics.table[TraceC][-7] = GFPORQ + FPORQ + PORQ + P
+    Semantics.table[TraceC][-6] = GFPORQ + FPORQ + NPORQ
+    Semantics.table[TraceC][-5] = GFPORQ + FPORQ + PORQ + PUQ + Q 
+}
+test_gfporq_semantics: assert {
+    wellformed_formulas
+    wellformed_traces
+    semantics
+    wellformed_example_gfporq 
+} 
+is sufficient for gfporq_semantics 
+for exactly 8 Formula, exactly 3 Trace