tla

package

v0.0.0-...-b9e74e0 Latest Latest Go to latest Published: Oct 19, 2022 License: Apache-2.0 Imports: 10 Imported by: 8

Details

Valid go.mod file

The Go module system was introduced in Go 1.11 and is the official dependency management solution for Go.
Redistributable license

Redistributable licenses place minimal restrictions on how software can be used, modified, and redistributed.
Tagged version

Modules with tagged versions give importers more predictable builds.
Stable version

When a project reaches major version v1 it is considered stable.
Learn more about best practices

Repository

github.com/UBC-NSS/pgo

Documentation ¶

Index ¶

Variables
type TLAFunctionSubstitutionRecord
type TLARecordField
- func (field TLARecordField) Hash() uint32
type TLAValue
type TLAValueHasher
- func (TLAValueHasher) Equal(a, b interface{}) bool
- func (TLAValueHasher) Hash(key interface{}) uint32

Constants ¶

This section is empty.

Variables ¶

View Source

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

View Source

var TLA_BOOLEAN = MakeTLASet(TLA_TRUE, TLA_FALSE)

View Source

var TLA_FALSE = TLAValue{tlaValueBool(false)}

View Source

var TLA_TRUE = TLAValue{tlaValueBool(true)}

View Source

var TLA_Zero = MakeTLANumber(0)

View Source

var TLA_defaultInitValue = TLAValue{}

Functions ¶

This section is empty.

Types ¶

type TLAFunctionSubstitutionRecord ¶

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

type TLARecordField ¶

type TLARecordField struct {
	Key, Value TLAValue
}

func (TLARecordField) Hash ¶

func (field TLARecordField) Hash() uint32

type TLAValue ¶

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

func MakeTLABool ¶

func MakeTLABool(v bool) TLAValue

func MakeTLAFunction ¶

func MakeTLAFunction(setVals []TLAValue, body func([]TLAValue) TLAValue) TLAValue

func MakeTLAFunctionSet ¶

func MakeTLAFunctionSet(from, to TLAValue) TLAValue

func MakeTLANumber ¶

func MakeTLANumber(num int32) TLAValue

func MakeTLARecord ¶

func MakeTLARecord(pairs []TLARecordField) TLAValue

func MakeTLARecordFromMap ¶

func MakeTLARecordFromMap(m *immutable.Map) TLAValue

func MakeTLARecordSet ¶

func MakeTLARecordSet(pairs []TLARecordField) TLAValue

func MakeTLASet ¶

func MakeTLASet(members ...TLAValue) TLAValue

func MakeTLASetFromMap ¶

func MakeTLASetFromMap(m *immutable.Map) TLAValue

func MakeTLAString ¶

func MakeTLAString(value string) TLAValue

func MakeTLATuple ¶

func MakeTLATuple(members ...TLAValue) TLAValue

func MakeTLATupleFromList ¶

func MakeTLATupleFromList(list *immutable.List) TLAValue

func TLAChoose ¶

func TLAChoose(setVal TLAValue, pred func(value TLAValue) bool) TLAValue

func TLACrossProduct ¶

func TLACrossProduct(vs ...TLAValue) TLAValue

func TLAFunctionSubstitution ¶

func TLAFunctionSubstitution(source TLAValue, substitutions []TLAFunctionSubstitutionRecord) TLAValue

func TLAQuantifiedExistential ¶

func TLAQuantifiedExistential(setVals []TLAValue, pred func([]TLAValue) bool) TLAValue

func TLAQuantifiedUniversal ¶

func TLAQuantifiedUniversal(setVals []TLAValue, pred func([]TLAValue) bool) TLAValue

func TLASetComprehension ¶

func TLASetComprehension(setVals []TLAValue, body func([]TLAValue) TLAValue) TLAValue

func TLASetRefinement ¶

func TLASetRefinement(setVal TLAValue, pred func(TLAValue) bool) TLAValue

func TLA_Append ¶

func TLA_Append(lhs, rhs TLAValue) TLAValue

func TLA_Assert ¶

func TLA_Assert(cond, msg TLAValue) TLAValue

func TLA_AsteriskSymbol ¶

func TLA_AsteriskSymbol(lhs, rhs TLAValue) TLAValue

func TLA_BackslashSymbol ¶

func TLA_BackslashSymbol(lhs, rhs TLAValue) TLAValue

func TLA_Cardinality ¶

func TLA_Cardinality(v TLAValue) TLAValue

func TLA_ColonGreaterThanSymbol ¶

func TLA_ColonGreaterThanSymbol(lhs, rhs TLAValue) TLAValue

func TLA_DivSymbol ¶

func TLA_DivSymbol(lhs, rhs TLAValue) TLAValue

func TLA_DomainSymbol ¶

func TLA_DomainSymbol(v TLAValue) TLAValue

func TLA_DotDotSymbol ¶

func TLA_DotDotSymbol(lhs, rhs TLAValue) TLAValue

func TLA_DoubleAtSignSymbol ¶

func TLA_DoubleAtSignSymbol(lhs, rhs TLAValue) TLAValue

func TLA_EqualsSymbol ¶

func TLA_EqualsSymbol(lhs, rhs TLAValue) TLAValue

func TLA_EquivSymbol ¶

func TLA_EquivSymbol(lhs, rhs TLAValue) TLAValue

func TLA_GreaterThanOrEqualSymbol ¶

func TLA_GreaterThanOrEqualSymbol(lhs, rhs TLAValue) TLAValue

func TLA_GreaterThanSymbol ¶

func TLA_GreaterThanSymbol(lhs, rhs TLAValue) TLAValue

func TLA_Head ¶

func TLA_Head(v TLAValue) TLAValue

func TLA_InSymbol ¶

func TLA_InSymbol(lhs, rhs TLAValue) TLAValue

func TLA_IntersectSymbol ¶

func TLA_IntersectSymbol(lhs, rhs TLAValue) TLAValue

func TLA_IsFiniteSet ¶

func TLA_IsFiniteSet(v TLAValue) TLAValue

func TLA_Len ¶

func TLA_Len(v TLAValue) TLAValue

func TLA_LessThanOrEqualSymbol ¶

func TLA_LessThanOrEqualSymbol(lhs, rhs TLAValue) TLAValue

func TLA_LessThanSymbol ¶

func TLA_LessThanSymbol(lhs, rhs TLAValue) TLAValue

func TLA_LogicalNotSymbol ¶

func TLA_LogicalNotSymbol(v TLAValue) TLAValue

func TLA_MinusSymbol ¶

func TLA_MinusSymbol(lhs, rhs TLAValue) TLAValue

func TLA_NegationSymbol ¶

func TLA_NegationSymbol(v TLAValue) TLAValue

func TLA_NotEqualsSymbol ¶

func TLA_NotEqualsSymbol(lhs, rhs TLAValue) TLAValue

func TLA_NotInSymbol ¶

func TLA_NotInSymbol(lhs, rhs TLAValue) TLAValue

func TLA_OSymbol ¶

func TLA_OSymbol(lhs, rhs TLAValue) TLAValue

func TLA_PercentSymbol ¶

func TLA_PercentSymbol(lhs, rhs TLAValue) TLAValue

func TLA_PlusSymbol ¶

func TLA_PlusSymbol(lhs, rhs TLAValue) TLAValue

func TLA_PrefixSubsetSymbol ¶

func TLA_PrefixSubsetSymbol(v TLAValue) TLAValue

func TLA_PrefixUnionSymbol ¶

func TLA_PrefixUnionSymbol(v TLAValue) TLAValue

func TLA_SelectSeq ¶

func TLA_SelectSeq(a, b TLAValue) TLAValue

TODO: TLA_SelectSeq, uses predicate

func TLA_Seq ¶

func TLA_Seq(v TLAValue) TLAValue

func TLA_SubSeq ¶

func TLA_SubSeq(v, m, n TLAValue) TLAValue

func TLA_SubsetOrEqualSymbol ¶

func TLA_SubsetOrEqualSymbol(lhs, rhs TLAValue) TLAValue

func TLA_SuperscriptSymbol ¶

func TLA_SuperscriptSymbol(lhs, rhs TLAValue) TLAValue

func TLA_Tail ¶

func TLA_Tail(v TLAValue) TLAValue

func TLA_ToString ¶

func TLA_ToString(value TLAValue) TLAValue

func TLA_UnionSymbol ¶

func TLA_UnionSymbol(lhs, rhs TLAValue) TLAValue

func (TLAValue) ApplyFunction ¶

func (v TLAValue) ApplyFunction(argument TLAValue) TLAValue

func (TLAValue) AsBool ¶

func (v TLAValue) AsBool() bool

func (TLAValue) AsFunction ¶

func (v TLAValue) AsFunction() *immutable.Map

func (TLAValue) AsNumber ¶

func (v TLAValue) AsNumber() int32

func (TLAValue) AsSet ¶

func (v TLAValue) AsSet() *immutable.Map

func (TLAValue) AsString ¶

func (v TLAValue) AsString() string

func (TLAValue) AsTuple ¶

func (v TLAValue) AsTuple() *immutable.List

func (TLAValue) Equal ¶

func (v TLAValue) Equal(other TLAValue) bool

func (*TLAValue) GobDecode ¶

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

func (*TLAValue) GobEncode ¶

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

func (TLAValue) Hash ¶

func (v TLAValue) Hash() uint32

func (TLAValue) IsBool ¶

func (v TLAValue) IsBool() bool

func (TLAValue) IsFunction ¶

func (v TLAValue) IsFunction() bool

func (TLAValue) IsNumber ¶

func (v TLAValue) IsNumber() bool

func (TLAValue) IsSet ¶

func (v TLAValue) IsSet() bool

func (TLAValue) IsString ¶

func (v TLAValue) IsString() bool

func (TLAValue) IsTuple ¶

func (v TLAValue) IsTuple() bool

func (TLAValue) PCalPrint ¶

func (v TLAValue) PCalPrint()

func (TLAValue) SelectElement ¶

func (v TLAValue) SelectElement(idx uint) TLAValue

func (TLAValue) String ¶

func (v TLAValue) String() string

type TLAValueHasher ¶

type TLAValueHasher struct{}

func (TLAValueHasher) Equal ¶

func (TLAValueHasher) Equal(a, b interface{}) bool

func (TLAValueHasher) Hash ¶

func (TLAValueHasher) Hash(key interface{}) uint32

Source Files ¶

View all Source files

?	: This menu
/	: Search site
f or F	: Jump to
y or Y	: Canonical URL