Packages

c

edu.cmu.cs.ls.keymaerax.tools.ext

MathematicaInvGenTool

class MathematicaInvGenTool extends BaseKeYmaeraMathematicaBridge[Expression] with InvGenTool with Logging

A continuous invariant implementation using Mathematica over the JLink interface.

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. MathematicaInvGenTool
  2. Logging
  3. LazyLogging
  4. LoggerHolder
  5. InvGenTool
  6. BaseKeYmaeraMathematicaBridge
  7. KeYmaeraMathematicaBridge
  8. AnyRef
  9. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new MathematicaInvGenTool(link: MathematicaLink)

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. val DEBUG: Boolean
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  5. val MEMORY_LIMIT_OFF: Long

    Default memory limit: no limit.

    Default memory limit: no limit.

    Definition Classes
    BaseKeYmaeraMathematicaBridge
  6. val TIMEOUT_OFF: Int

    Default timeout for Mathematica requests: no timeout.

    Default timeout for Mathematica requests: no timeout.

    Definition Classes
    BaseKeYmaeraMathematicaBridge
  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. def availableWorkers: Int
  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  10. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  11. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  12. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  13. def genODECond(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): (List[Formula], List[Formula])

    Returns the sufficient/necessary condition for postCond to be invariant (left of pair) also returns necessary conditions for the safety question to be true at all with those assumptions (right of pair) In either case, all formulas in the returned list must be valid

    Returns the sufficient/necessary condition for postCond to be invariant (left of pair) also returns necessary conditions for the safety question to be true at all with those assumptions (right of pair) In either case, all formulas in the returned list must be valid

    Definition Classes
    MathematicaInvGenToolInvGenTool
  14. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  15. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  16. def init(): Boolean
  17. def invgen(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): Seq[Either[Seq[(Formula, String)], Seq[(Formula, String)]]]

    Returns a continuous invariant for a safety problem sent to the tool.

    Returns a continuous invariant for a safety problem sent to the tool.

    ode

    The differential equation for which to generate a continuous invariants.

    assumptions

    Assumptions on the initial state of the ODE.

    postCond

    What to prove from the invariants.

    returns

    A sequence of continuous invariants, each to be proved with a diffcut chain (left=invariant, right=candidate).

    Definition Classes
    MathematicaInvGenToolInvGenTool
  18. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  19. val k2m: K2MConverter[Expression]
  20. val link: MathematicaLink
  21. lazy val logger: Logger
    Attributes
    protected
    Definition Classes
    LazyLogging → LoggerHolder
  22. final val loggerName: String
    Attributes
    protected
    Definition Classes
    LoggerHolder
  23. def lzzCheck(ode: ODESystem, inv: Formula): Boolean

    Fast check whether or not inv is worth proving to be an invariant of ode.

    Fast check whether or not inv is worth proving to be an invariant of ode.

    Definition Classes
    MathematicaInvGenToolInvGenTool
  24. val m2k: M2KConverter[Expression]
  25. var mathematicaExecutor: ToolExecutor
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  26. def memoryConstrained(cmd: String): String
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  27. def memoryConstrained(cmd: MExpr): MExpr
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  28. var memoryLimit: Long

    Memory limit for Mathematica requests in MB, set to MEMORY_LIMIT_OFF to disable.

    Memory limit for Mathematica requests in MB, set to MEMORY_LIMIT_OFF to disable.

    Definition Classes
    BaseKeYmaeraMathematicaBridge
  29. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  30. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  31. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  32. def problemClassification(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): (Int, String, Map[String, Map[String, String]])

    Returns dimension and classification of the problem defined by ode with assumptions assumptions and postcondition postCond.

    Returns dimension and classification of the problem defined by ode with assumptions assumptions and postcondition postCond.

    ode

    The differential equation system including evolution domain constraint.

    assumptions

    Assumptions on the initial state.

    postCond

    Postcondition

    returns

    The dimension and classification of the problem.

  33. def refuteODE(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): Option[Map[NamedSymbol, Expression]]

    Finds counterexamples to an ODE safety conjecture.

    Finds counterexamples to an ODE safety conjecture.

    Definition Classes
    MathematicaInvGenToolInvGenTool
  34. def run(cmd: MExpr): (String, Expression)

    Runs Mathematica command cmd, with Mathematica exception checking.

    Runs Mathematica command cmd, with Mathematica exception checking.

    Definition Classes
    BaseKeYmaeraMathematicaBridgeKeYmaeraMathematicaBridge
  35. def runUnchecked(cmd: String): (String, Expression)

    Runs Mathematica command cmd without safeguarding by exception checking for Mathematica results.

    Runs Mathematica command cmd without safeguarding by exception checking for Mathematica results.

    Definition Classes
    BaseKeYmaeraMathematicaBridgeKeYmaeraMathematicaBridge
  36. def shutdown(): Unit
  37. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  38. def timeConstrained(cmd: String): String
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  39. def timeConstrained(cmd: MExpr): MExpr
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  40. var timeout: Int

    Timeout for Mathematica requests in seconds, set to TIMEOUT_OFF to disable.

    Timeout for Mathematica requests in seconds, set to TIMEOUT_OFF to disable.

    Definition Classes
    BaseKeYmaeraMathematicaBridge
  41. def toString(): String
    Definition Classes
    AnyRef → Any
  42. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  43. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  44. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Logging

Inherited from LazyLogging

Inherited from LoggerHolder

Inherited from InvGenTool

Inherited from AnyRef

Inherited from Any

Ungrouped