object LTLClosures
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- LTLClosures
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- All
Type Members
- type LTLContext[G, M] = MatrixContext[G, LTLformula[M]]
- case class LTLalways[M](formula: LTLformula[M]) extends LTLformula[M] with Product with Serializable
- case class LTLconjunction[M](conjuncts: Iterable[LTLformula[M]]) extends LTLformula[M] with Product with Serializable
- abstract class LTLformula[+M] extends AnyRef
- case class LTLimplication[M](premise: LTLformula[M], conclusion: LTLformula[M]) extends LTLformula[M] with Product with Serializable
- case class LTLliteral[M](variable: M) extends LTLformula[M] with Product with Serializable
- case class LTLnext[M](formula: LTLformula[M]) extends LTLformula[M] with Product with Serializable
- case class LTLsometimes[M](formula: LTLformula[M]) extends LTLformula[M] with Product with Serializable
- case class LTLuntil[M](guard: LTLformula[M], future: LTLformula[M]) extends LTLformula[M] with Product with Serializable
- type TemporalContext[G, M] = MatrixContext[G, (M, Int)]
- type Trace[M] = Set[(M, Int)]
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
- def fromJavaSet[T](jset: Set[T]): Set[T]
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- def getObjectTrace[G, M](cxt: MatrixContext[G, (M, Int)], obj: G): Trace[M]
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def ltlize[G, M](tcxt: TemporalContext[G, M], t0: Int): LTLContext[G, M]
- def ltlmodels[G, M](tcxt: TemporalContext[G, M], tmax: Int)(g: G, t: Int, ƒ: LTLformula[M]): Boolean
- def main(args: Array[String]): Unit
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
- def temporalContext[G, M](data: (G, M, Int)*): TemporalContext[G, M]
- def toJavaSet[T](set: Set[T]): Set[T]
- def toLTLformula[M](trace: Trace[M], t0: Int, t1: Int, depth: Int): LTLformula[M]
- def toLTLformula[M](trace: Trace[M], t0: Int, depth: Int): LTLformula[M]
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
- object LTLfalse extends LTLformula[Nothing] with Product with Serializable
- object LTLtrue extends LTLformula[Nothing] with Product with Serializable