package ltl
- Alphabetic
- Public
- Protected
Type Members
- sealed abstract class AssertPropertyLike extends AnyRef
The base class for the
AssertProperty,AssumeProperty, andCoverPropertyverification constructs.The base class for the
AssertProperty,AssumeProperty, andCoverPropertyverification constructs.- Annotations
- @nowarn()
- sealed trait Property extends AnyRef
A Linear Temporal Logic (LTL) property.
- sealed trait Sequence extends Property
A Linear Temporal Logic (LTL) sequence.
- sealed trait SequenceAtom extends AnyRef
A single item that may be used in the
Sequence(...)convenience constructor for sequences.A single item that may be used in the
Sequence(...)convenience constructor for sequences. These atoms may either beSequences themselves, likeaora and b, or aDelayAtom, likeDelay. Together they enable a shorthand notation for sequences like:Sequence(a, Delay(), b, Delay(2), c, Delay(3, 9), d, Delay(4, None), e).
Value Members
- object AssertProperty extends AssertPropertyLike
Assert that a property holds.
Assert that a property holds.
Use like
AssertProperty(p). SeeAssertPropertyLike.applyfor optional clock, disable_iff, and label parameters. - object AssumeProperty extends AssertPropertyLike
Assume that a property holds.
Assume that a property holds.
Use like
AssumeProperty(p). SeeAssertPropertyLike.applyfor optional clock, disable_iff, and label parameters. - object CoverProperty extends AssertPropertyLike
Cover that a property holds.
Cover that a property holds.
Use like
CoverProperty(p). SeeAssertPropertyLike.applyfor optional clock, disable_iff, and label parameters. - object Delay
The delay atoms available to users.
The delay atoms available to users. Can be interleaved with actual sequences in
Sequence(...). SeeSequenceAtomfor details. - object Property
Prefix-style utilities to work with properties.
Prefix-style utilities to work with properties.
This object exposes the primary API to create and compose properties from booleans, sequences, and other properties.
- object Sequence
Prefix-style utilities to work with sequences.
Prefix-style utilities to work with sequences.
This object exposes the primary API to create and compose sequences from booleans and shorter sequences.