mirror of
https://github.com/priyanshujain/sanderling.git
synced 2026-10-02 11:07:10 +00:00
pj
0c277b2833
Supports Always over Pure/Thunk leaves; eventually/next/bounds deferred. Once a thunk returns false under an Always, the verdict latches to violated so the runner can surface the offending step without later observations masking it.
41 lines
1.1 KiB
Go
41 lines
1.1 KiB
Go
package ltl
|
|
|
|
import "fmt"
|
|
|
|
// Formula is the AST of a temporal logic property. v0.1 supports only Always
|
|
// over Pure/Thunk leaves; eventually, next, and bounded operators are
|
|
// deferred to v0.2+.
|
|
type Formula interface {
|
|
isFormula()
|
|
describe() string
|
|
}
|
|
|
|
type AlwaysFormula struct {
|
|
Inner Formula
|
|
}
|
|
|
|
type PureFormula struct {
|
|
Value bool
|
|
}
|
|
|
|
type ThunkFormula struct {
|
|
Func func() bool
|
|
}
|
|
|
|
func Always(inner Formula) Formula { return AlwaysFormula{Inner: inner} }
|
|
|
|
func Pure(value bool) Formula { return PureFormula{Value: value} }
|
|
|
|
func Thunk(function func() bool) Formula { return ThunkFormula{Func: function} }
|
|
|
|
func (AlwaysFormula) isFormula() {}
|
|
func (PureFormula) isFormula() {}
|
|
func (ThunkFormula) isFormula() {}
|
|
|
|
func (a AlwaysFormula) describe() string { return "Always(" + a.Inner.describe() + ")" }
|
|
func (p PureFormula) describe() string { return fmt.Sprintf("Pure(%t)", p.Value) }
|
|
func (ThunkFormula) describe() string { return "Thunk(...)" }
|
|
|
|
// Describe returns a debug-friendly representation of the formula.
|
|
func Describe(formula Formula) string { return formula.describe() }
|