itf

Documentation

Index

• type Expr
  • func (e *Expr) UnmarshalJSON(data []byte) error
• type ListExprType
• type MapExprType
• type State
  • func (s *State) UnmarshalJSON(data []byte) error
• type Trace
  • func (trace *Trace) LoadFromFile(filePath string) error

Types

type Expr

type Expr struct {
	Value any
}

func (*Expr) UnmarshalJSON

func (e *Expr) UnmarshalJSON(data []byte) error

type ListExprType

type ListExprType = []Expr

type MapExprType

type MapExprType = map[string]Expr

type State

type State struct {
	Meta      map[string]any   `json:"#meta,omitempty"`
	VarValues map[string]*Expr `json:",omitempty"`
}

func (*State) UnmarshalJSON

func (s *State) UnmarshalJSON(data []byte) error

type Trace

type Trace struct {
	Meta   *meta            `json:"#meta,omitempty"`
	Params map[string]*Expr `json:"params"`
	Vars   []string         `json:"vars"`
	States []*State         `json:"states"`
	Loop   int              `json:"loop,omitempty"`
}

ITF spec: https://apalache.informal.systems/docs/adr/015adr-trace.html#the-itf-format

func (*Trace) LoadFromFile

func (trace *Trace) LoadFromFile(filePath string) error