Documentation
¶
Index ¶
- func ComparePredicateID(a, b IRPredicateID) int
- func ComparePredicateWithID(a, b IRPredicateWithID) int
- func FormatPredicateID(id IRPredicateID) string
- func HasVars(ir IRLivelockFree) bool
- type IRArg
- type IRConst
- type IREdge
- type IRField
- type IRInit
- type IRLivelockFree
- type IRPredicate
- type IRPredicateID
- type IRPredicateWithID
- type IRState
- type IRStateWithID
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func ComparePredicateID ¶
func ComparePredicateID(a, b IRPredicateID) int
func ComparePredicateWithID ¶
func ComparePredicateWithID(a, b IRPredicateWithID) int
func FormatPredicateID ¶
func FormatPredicateID(id IRPredicateID) string
FormatPredicateID renders an ID as the base-36 suffix of a generated predicate name (pred_<id>). Every backend must name a given predicate identically, so this is the single definition of that spelling.
func HasVars ¶
func HasVars(ir IRLivelockFree) bool
HasVars reports whether any state has a variable, in which case the json datatype is emitted (otherwise it would be unused).
Types ¶
type IRArg ¶
type IRArg struct {
Name string `json:"name"`
Type string `json:"type"`
Primed bool `json:"primed"`
}
IRArg is one argument of a predicate (an event parameter or a state variable). Primed marks a post-state variable.
type IREdge ¶
type IREdge struct {
Src csdf.StateID `json:"src"`
Dst csdf.StateID `json:"dst"`
Event csdf.Event `json:"event"`
EventParams []IRArg `json:"event_params"`
Guard IRPredicateID `json:"guard"`
Post IRPredicateID `json:"post"`
Line int `json:"line"` // 1-based
}
IREdge is one transition. Guard/Post hold either a predicate symbol or the literal "True" when the predicate is omitted.
type IRInit ¶
type IRInit struct {
Dst csdf.StateID `json:"state"`
Post IRPredicateID `json:"post"`
Line int `json:"line"` // 1-based
}
IRInit names the start state.
type IRLivelockFree ¶
type IRLivelockFree struct {
// Structurally is true when no reachable τ-only cycle exists, in which case
// the obligation holds regardless of the predicates.
Structurally bool `json:"structurally"`
Predicates map[IRPredicateID]IRPredicate `json:"predicates"`
States map[csdf.StateID]IRState `json:"states"` // the state space as an ADT
Constants []IRConst `json:"constants"` // global opaque constants in scope
Edges []IREdge `json:"edges"` // the labelled transitions
Init IRInit `json:"init"`
}
IRLivelockFree is a prover-agnostic intermediate representation of the proof obligation that the diagram is livelock free, i.e. no reachable state admits an infinite run of internal (τ) transitions. Natural-language Guard/Post predicates are left opaque, deduplicated into Predicates under the hash of their text and argument types; an edge names one by id. A downstream generator expands this IR into Lean or Isabelle, and the predicate bodies are supplied separately. Both are out of scope here.
func BuildLivelockFree ¶
func BuildLivelockFree(d *csdf.Diagram) IRLivelockFree
BuildLivelockFree builds the livelock-freedom proof obligation IR for d. The structural τ-cycle check (CheckLivelockFree) is used only to set StructurallyLivelockFree; the obligation itself is the global property and does not depend on a particular witness.
type IRPredicate ¶
IRPredicate is an opaque predicate symbol with its argument signature and the verbatim natural-language text it stands for. Kind is "guard", "post", or "init".
func (IRPredicate) Hash ¶
func (p IRPredicate) Hash(h hash.Hash32) IRPredicateID
func (IRPredicate) WithID ¶
func (p IRPredicate) WithID(h hash.Hash32) IRPredicateWithID
type IRPredicateID ¶
type IRPredicateID uint32
type IRPredicateWithID ¶
type IRPredicateWithID struct {
ID IRPredicateID `json:"hash"`
Predicate IRPredicate `json:"predicate"`
}
func IRPredicatesWithHash ¶
func IRPredicatesWithHash(ps []IRPredicate) []IRPredicateWithID
func Predicates ¶
func Predicates(ps map[IRPredicateID]IRPredicate) []IRPredicateWithID
type IRStateWithID ¶
func SortIRStates ¶
func SortIRStates(m map[csdf.StateID]IRState) []IRStateWithID
Source Files
Directories
¶
| Path | Synopsis |
|---|---|
|
Package json compiles the livelock-freedom obligation IR to its JSON encoding (the "ir-json" target), the canonical wire form also emitted by csdflivelockfree.
|
Package json compiles the livelock-freedom obligation IR to its JSON encoding (the "ir-json" target), the canonical wire form also emitted by csdflivelockfree. |
|
Package isabelle compiles the livelock-freedom obligation IR to an Isabelle/HOL proof obligation skeleton.
|
Package isabelle compiles the livelock-freedom obligation IR to an Isabelle/HOL proof obligation skeleton. |
|
Package lean compiles the livelock-freedom obligation IR to a Lean 4 proof obligation skeleton.
|
Package lean compiles the livelock-freedom obligation IR to a Lean 4 proof obligation skeleton. |
|
Package target dispatches the livelock-freedom obligation IR to a prover backend by target name, so every command exposes the same set of -target values and routes them the same way.
|
Package target dispatches the livelock-freedom obligation IR to a prover backend by target name, so every command exposes the same set of -target values and routes them the same way. |