tla

Documentation

Index

• Variables
• type FunctionSubstitutionRecord
• type RecordField
  • func (field RecordField) Hash() uint32
• type Value
  • func Choose(setVal Value, pred func(value Value) bool) Value
  • func CrossProduct(vs ...Value) Value
  • func FunctionSubstitution(source Value, substitutions []FunctionSubstitutionRecord) Value
  • func MakeBool(v bool) Value
  • func MakeFunction(setVals []Value, body func([]Value) Value) Value
  • func MakeFunctionSet(from, to Value) Value
  • func MakeNumber(num int32) Value
  • func MakeRecord(pairs []RecordField) Value
  • func MakeRecordFromMap(m *immutable.Map[Value, Value]) Value
  • func MakeRecordSet(pairs []RecordField) Value
  • func MakeSet(members ...Value) Value
  • func MakeSetFromMap(m *immutable.Map[Value, bool]) Value
  • func MakeString(value string) Value
  • func MakeTuple(members ...Value) Value
  • func MakeTupleFromList(list *immutable.List[Value]) Value
  • func ModuleAppend(lhs, rhs Value) Value
  • func ModuleAssert(cond, msg Value) Value
  • func ModuleAsteriskSymbol(lhs, rhs Value) Value
  • func ModuleBackslashSymbol(lhs, rhs Value) Value
  • func ModuleCardinality(v Value) Value
  • func ModuleColonGreaterThanSymbol(lhs, rhs Value) Value
  • func ModuleDivSymbol(lhs, rhs Value) Value
  • func ModuleDomainSymbol(v Value) Value
  • func ModuleDotDotSymbol(lhs, rhs Value) Value
  • func ModuleDoubleAtSignSymbol(lhs, rhs Value) Value
  • func ModuleEqualsSymbol(lhs, rhs Value) Value
  • func ModuleEquivSymbol(lhs, rhs Value) Value
  • func ModuleGreaterThanOrEqualSymbol(lhs, rhs Value) Value
  • func ModuleGreaterThanSymbol(lhs, rhs Value) Value
  • func ModuleHead(v Value) Value
  • func ModuleInSymbol(lhs, rhs Value) Value
  • func ModuleIntersectSymbol(lhs, rhs Value) Value
  • func ModuleIsFiniteSet(v Value) Value
  • func ModuleLen(v Value) Value
  • func ModuleLessThanOrEqualSymbol(lhs, rhs Value) Value
  • func ModuleLessThanSymbol(lhs, rhs Value) Value
  • func ModuleLogicalNotSymbol(v Value) Value
  • func ModuleMinusSymbol(lhs, rhs Value) Value
  • func ModuleNegationSymbol(v Value) Value
  • func ModuleNotEqualsSymbol(lhs, rhs Value) Value
  • func ModuleNotInSymbol(lhs, rhs Value) Value
  • func ModuleOSymbol(lhs, rhs Value) Value
  • func ModulePercentSymbol(lhs, rhs Value) Value
  • func ModulePlusSymbol(lhs, rhs Value) Value
  • func ModulePrefixSubsetSymbol(v Value) Value
  • func ModulePrefixUnionSymbol(v Value) Value
  • func ModuleSelectSeq(a, b Value) Value
  • func ModuleSeq(v Value) Value
  • func ModuleSubSeq(v, m, n Value) Value
  • func ModuleSubsetOrEqualSymbol(lhs, rhs Value) Value
  • func ModuleSuperscriptSymbol(lhs, rhs Value) Value
  • func ModuleTail(v Value) Value
  • func ModuleToString(value Value) Value
  • func ModuleUnionSymbol(lhs, rhs Value) Value
  • func QuantifiedExistential(setVals []Value, pred func([]Value) bool) Value
  • func QuantifiedUniversal(setVals []Value, pred func([]Value) bool) Value
  • func SetComprehension(setVals []Value, body func([]Value) Value) Value
  • func SetRefinement(setVal Value, pred func(Value) bool) Value
  • func (v Value) ApplyFunction(argument Value) Value
  • func (v Value) AsBool() bool
  • func (v Value) AsFunction() *immutable.Map[Value, Value]
  • func (v Value) AsNumber() int32
  • func (v Value) AsSet() *immutable.Map[Value, bool]
  • func (v Value) AsString() string
  • func (v Value) AsTuple() *immutable.List[Value]
  • func (v Value) Equal(other Value) bool
  • func (v *Value) GobDecode(input []byte) error
  • func (v *Value) GobEncode() ([]byte, error)
  • func (v Value) Hash() uint32
  • func (v Value) IsBool() bool
  • func (v Value) IsFunction() bool
  • func (v Value) IsNumber() bool
  • func (v Value) IsSet() bool
  • func (v Value) IsString() bool
  • func (v Value) IsTuple() bool
  • func (v Value) PCalPrint()
  • func (v Value) SelectElement(idx uint) Value
  • func (v Value) String() string
• type ValueHasher
  • func (ValueHasher) Equal(a, b Value) bool
  • func (ValueHasher) Hash(key Value) uint32

Variables

var ErrTLAType = errors.New("TLA+ type error")

var ModuleBOOLEAN = MakeSet(ModuleTRUE, ModuleFALSE)

var ModuleFALSE = Value{valueBool(false)}

var ModuleTRUE = Value{valueBool(true)}

var ModuleZero = MakeNumber(0)

var ModuledefaultInitValue = Value{}

Types

type FunctionSubstitutionRecord

type FunctionSubstitutionRecord struct {
	Keys  []Value
	Value func(anchor Value) Value
}

type RecordField

type RecordField struct {
	Key, Value Value
}

func (RecordField) Hash

func (field RecordField) Hash() uint32

type Value

type Value struct {
	// contains filtered or unexported fields
}

func Choose

func Choose(setVal Value, pred func(value Value) bool) Value

func CrossProduct

func CrossProduct(vs ...Value) Value

func FunctionSubstitution

func FunctionSubstitution(source Value, substitutions []FunctionSubstitutionRecord) Value

func MakeBool

func MakeBool(v bool) Value

func MakeFunction

func MakeFunction(setVals []Value, body func([]Value) Value) Value

func MakeFunctionSet

func MakeFunctionSet(from, to Value) Value

func MakeNumber

func MakeNumber(num int32) Value

func MakeRecord

func MakeRecord(pairs []RecordField) Value

func MakeRecordFromMap

func MakeRecordFromMap(m *immutable.Map[Value, Value]) Value

func MakeRecordSet

func MakeRecordSet(pairs []RecordField) Value

func MakeSet

func MakeSet(members ...Value) Value

func MakeSetFromMap

func MakeSetFromMap(m *immutable.Map[Value, bool]) Value

func MakeString

func MakeString(value string) Value

func MakeTuple

func MakeTuple(members ...Value) Value

func MakeTupleFromList

func MakeTupleFromList(list *immutable.List[Value]) Value

func ModuleAppend

func ModuleAppend(lhs, rhs Value) Value

func ModuleAssert

func ModuleAssert(cond, msg Value) Value

func ModuleAsteriskSymbol

func ModuleAsteriskSymbol(lhs, rhs Value) Value

func ModuleBackslashSymbol

func ModuleBackslashSymbol(lhs, rhs Value) Value

func ModuleCardinality

func ModuleCardinality(v Value) Value

func ModuleColonGreaterThanSymbol

func ModuleColonGreaterThanSymbol(lhs, rhs Value) Value

func ModuleDivSymbol

func ModuleDivSymbol(lhs, rhs Value) Value

func ModuleDomainSymbol

func ModuleDomainSymbol(v Value) Value

func ModuleDotDotSymbol

func ModuleDotDotSymbol(lhs, rhs Value) Value

func ModuleDoubleAtSignSymbol

func ModuleDoubleAtSignSymbol(lhs, rhs Value) Value

func ModuleEqualsSymbol

func ModuleEqualsSymbol(lhs, rhs Value) Value

func ModuleEquivSymbol

func ModuleEquivSymbol(lhs, rhs Value) Value

func ModuleGreaterThanOrEqualSymbol

func ModuleGreaterThanOrEqualSymbol(lhs, rhs Value) Value

func ModuleGreaterThanSymbol

func ModuleGreaterThanSymbol(lhs, rhs Value) Value

func ModuleHead

func ModuleHead(v Value) Value

func ModuleInSymbol

func ModuleInSymbol(lhs, rhs Value) Value

func ModuleIntersectSymbol

func ModuleIntersectSymbol(lhs, rhs Value) Value

func ModuleIsFiniteSet

func ModuleIsFiniteSet(v Value) Value

func ModuleLen

func ModuleLen(v Value) Value

func ModuleLessThanOrEqualSymbol

func ModuleLessThanOrEqualSymbol(lhs, rhs Value) Value

func ModuleLessThanSymbol

func ModuleLessThanSymbol(lhs, rhs Value) Value

func ModuleLogicalNotSymbol

func ModuleLogicalNotSymbol(v Value) Value

func ModuleMinusSymbol

func ModuleMinusSymbol(lhs, rhs Value) Value

func ModuleNegationSymbol

func ModuleNegationSymbol(v Value) Value

func ModuleNotEqualsSymbol

func ModuleNotEqualsSymbol(lhs, rhs Value) Value

func ModuleNotInSymbol

func ModuleNotInSymbol(lhs, rhs Value) Value

func ModuleOSymbol

func ModuleOSymbol(lhs, rhs Value) Value

func ModulePercentSymbol

func ModulePercentSymbol(lhs, rhs Value) Value

func ModulePlusSymbol

func ModulePlusSymbol(lhs, rhs Value) Value

func ModulePrefixSubsetSymbol

func ModulePrefixSubsetSymbol(v Value) Value

func ModulePrefixUnionSymbol

func ModulePrefixUnionSymbol(v Value) Value

func ModuleSelectSeq

func ModuleSelectSeq(a, b Value) Value

TODO: ModuleSelectSeq, uses predicate

func ModuleSeq

func ModuleSeq(v Value) Value

func ModuleSubSeq

func ModuleSubSeq(v, m, n Value) Value

func ModuleSubsetOrEqualSymbol

func ModuleSubsetOrEqualSymbol(lhs, rhs Value) Value

func ModuleSuperscriptSymbol

func ModuleSuperscriptSymbol(lhs, rhs Value) Value

func ModuleTail

func ModuleTail(v Value) Value

func ModuleToString

func ModuleToString(value Value) Value

func ModuleUnionSymbol

func ModuleUnionSymbol(lhs, rhs Value) Value

func QuantifiedExistential

func QuantifiedExistential(setVals []Value, pred func([]Value) bool) Value

func QuantifiedUniversal

func QuantifiedUniversal(setVals []Value, pred func([]Value) bool) Value

func SetComprehension

func SetComprehension(setVals []Value, body func([]Value) Value) Value

func SetRefinement

func SetRefinement(setVal Value, pred func(Value) bool) Value

func (Value) ApplyFunction

func (v Value) ApplyFunction(argument Value) Value

func (Value) AsBool

func (v Value) AsBool() bool

func (Value) AsFunction

func (v Value) AsFunction() *immutable.Map[Value, Value]

func (Value) AsNumber

func (v Value) AsNumber() int32

func (Value) AsSet

func (v Value) AsSet() *immutable.Map[Value, bool]

func (Value) AsString

func (v Value) AsString() string

func (Value) AsTuple

func (v Value) AsTuple() *immutable.List[Value]

func (Value) Equal

func (v Value) Equal(other Value) bool

func (*Value) GobDecode

func (v *Value) GobDecode(input []byte) error

func (*Value) GobEncode

func (v *Value) GobEncode() ([]byte, error)

func (Value) Hash

func (v Value) Hash() uint32

func (Value) IsBool

func (v Value) IsBool() bool

func (Value) IsFunction

func (v Value) IsFunction() bool

func (Value) IsNumber

func (v Value) IsNumber() bool

func (Value) IsSet

func (v Value) IsSet() bool

func (Value) IsString

func (v Value) IsString() bool

func (Value) IsTuple

func (v Value) IsTuple() bool

func (Value) PCalPrint

func (v Value) PCalPrint()

func (Value) SelectElement

func (v Value) SelectElement(idx uint) Value

func (Value) String

func (v Value) String() string

type ValueHasher

type ValueHasher struct{}

func (ValueHasher) Equal

func (ValueHasher) Equal(a, b Value) bool

func (ValueHasher) Hash

func (ValueHasher) Hash(key Value) uint32