From 5bf23585f30cab864dbbcf5bfdaec3f15a48521c Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Mon, 24 Feb 2025 14:14:41 -0500 Subject: [PATCH] add: ltlf model draft example --- forge/examples/README.md | 6 +- forge/examples/ltlf/README.md | 6 ++ forge/examples/ltlf/ltl_f.frg | 162 +++++++++++++++++++++++++++++ forge/examples/ltlf/ltl_f.test.frg | 94 +++++++++++++++++ 4 files changed, 267 insertions(+), 1 deletion(-) create mode 100644 forge/examples/ltlf/README.md create mode 100644 forge/examples/ltlf/ltl_f.frg create mode 100644 forge/examples/ltlf/ltl_f.test.frg diff --git a/forge/examples/README.md b/forge/examples/README.md index b23d4593..ceb0cec6 100644 --- a/forge/examples/README.md +++ b/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. diff --git a/forge/examples/ltlf/README.md b/forge/examples/ltlf/README.md new file mode 100644 index 00000000..acb04283 --- /dev/null +++ b/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. + diff --git a/forge/examples/ltlf/ltl_f.frg b/forge/examples/ltlf/ltl_f.frg new file mode 100644 index 00000000..37c6682e --- /dev/null +++ b/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 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 diff --git a/forge/examples/ltlf/ltl_f.test.frg b/forge/examples/ltlf/ltl_f.test.frg new file mode 100644 index 00000000..a54991a5 --- /dev/null +++ b/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 \ No newline at end of file