formula

type Bool ¶

type Bool int

Bool is the type of ternary Boolean values (True, False, Undef). By construction, the zero value of a Bool is UNDEF.

const (
	UNDEF Bool = 0
	FALSE Bool = 1
	TRUE  Bool = 2
)

func BoolAnd(b1, b2 Bool) Bool

func BoolIff(b1, b2 Bool) Bool

func BoolNot(b Bool) Bool

func BoolOr(b1, b2 Bool) Bool

func FoldAnd[T any](f func(T) Bool, bs []T) Bool

func FoldOr[T any](f func(T) Bool, bs []T) Bool

func NewBool(b bool) Bool

func (b Bool) EqualTo(b2 bool) bool

func (b Bool) If(f func(bool))

func (b Bool) IsFalse() bool

func (b Bool) IsTrue() bool

func (b Bool) PrintShort() string

func (b Bool) String() string

func (b Bool) Value() (bool, bool)

type BooleanConstant ¶

type BooleanConstant bool

BooleanConstant defines a constant True or False.

func (f BooleanConstant) String() string

type Conjunction ¶

type Conjunction []Formula

Conjunction is the conjunction of two or more formulas.

func (f Conjunction) String() string

type Constant ¶

type Constant struct {
	Value []byte `xml:",innerxml"`
}

type Decoder ¶

type Decoder struct {
	*xml.Decoder
}

A Decoder represents an XML parser reading a particular input stream that should be a valid formula file. It embeds an xml.Decoder for parsing a XML stream passed as an io.Reader. Like with xml.Decoder, the parser assumes that its input is encoded in UTF-8.

func NewDecoder(r io.Reader) *Decoder

func (d *Decoder) Build() ([]Query, error)

type Disjunction ¶

type Disjunction []Formula

Disjunction is the disjunction of two or more formulas.

func (f Disjunction) String() string

type Formula ¶

type Formula interface {
	String() string
}

Formula is the interface that wraps the type of XML Formula.

Includes reports if one of the constant in the formula is part of the set of names

func Simplify(f Formula) Formula

type IntegerConstant ¶

type IntegerConstant int

IntegerConstant defines an integer constant. It is an atomic integer expression.

func (f IntegerConstant) String() string

type IntegerLe ¶

type IntegerLe struct {
	Left  Formula
	Right Formula
}

IntegerLe returns true if the value of the Left integer expression is less than or equal to the value of the Right one.

func (f IntegerLe) String() string

type IsFireable ¶

type IsFireable []string

IsFireable evaluates to true if one of the declared transition is fireable.

func (f IsFireable) String() string

type Negation ¶

type Negation struct {
	Formula
}

Negation is the type of all expressions.

func (f Negation) String() string

type Places ¶

type Places struct {
	PlList []string `xml:"place"`
}

type Property ¶

type Property struct {
	Id string `xml:"id"`
	EF RawXML `xml:"formula>exists-path>finally,omitempty"`
	AG RawXML `xml:"formula>all-paths>globally,omitempty"`
}

Property is one of EF phi or AG phi, with phi a state formula

type PropertySet ¶

type PropertySet struct {
	XMLName xml.Name   `xml:"property-set"`
	List    []Property `xml:"property"`
}

PropertySet is the type of set of formulas defined in a MCC XML property file. We should have a list of 16 properties included inside a `property-set` XML element.

type Query ¶

type Query struct {
	ID             string
	IsEF           bool
	IsReachability bool
	Skip           bool    // whether we should skip evaluating this formula
	Original       Formula // formula before simplification. For debugging purpose
	Formula
}

Query is the type of reachability queries we need to check. When IsEF is true the query is (EF phi), meaning we report true if we can reach a state where phi is true. Conversely, when IsEF is false, the query is (AG phi), meaning we report false if (not phi) is reachable.

func (q Query) IsTrivial() bool

func (p Query) String() string

type RawXML ¶

type RawXML struct {
	InnerXML []byte `xml:",innerxml"`
}

StateFormula is a Boolean combination of atomic properties and integer expressions that we should parse explicitly.

type TokensCount ¶

type TokensCount []string

TokensCount returns the exact number of tokens in a set of places. It is an atomic integer expression.

func (f TokensCount) String() string

type Transitions ¶

type Transitions struct {
	TrList []string `xml:"transition"`
}