Packages

c

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

TestSynthesis

class TestSynthesis extends BaseKeYmaeraMathematicaBridge[Either[KExpr, NamedSymbol]]

Synthesize test case configurations from ModelPlex formulas. Requires Mathematica.

Created by smitsch on 12/6/16.

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TestSynthesis
  2. BaseKeYmaeraMathematicaBridge
  3. KeYmaeraMathematicaBridge
  4. AnyRef
  5. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new TestSynthesis(mathematicaTool: Mathematica)

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. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. def getSafetyRange(fml: Formula): (Number, Number)

    Computes the maximum safety range of fml.

  15. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  16. def init(): Boolean
  17. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  18. val k2m: K2MConverter[Either[KExpr, NamedSymbol]]
  19. val link: MathematicaLink
  20. val m2k: M2KConverter[Either[KExpr, NamedSymbol]]
  21. var mathematicaExecutor: ToolExecutor
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  22. def memoryConstrained(cmd: String): String
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  23. def memoryConstrained(cmd: MExpr): MExpr
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  24. 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
  25. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  26. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  27. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  28. def run(cmd: MExpr): (String, Either[KExpr, NamedSymbol])

    Runs Mathematica command cmd, with Mathematica exception checking.

    Runs Mathematica command cmd, with Mathematica exception checking.

    Definition Classes
    BaseKeYmaeraMathematicaBridgeKeYmaeraMathematicaBridge
  29. def runUnchecked(cmd: String): (String, Either[KExpr, NamedSymbol])

    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
  30. def shutdown(): Unit
  31. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  32. def synthesizeSafetyMarginCheck(fml: Formula, vals: Map[Term, Term]): Number

    Synthesize a safety margin check, 0 is the boundary between safe and unsafe, positive values indicate unsafety, negative values safety.

  33. def synthesizeTestConfig(fml: Formula, amount: Int = 1, timeout: Option[Int] = None, safetyMargin: Option[(Number, Number)] = None): List[Map[Term, Term]]

    Synthesize test configurations of both initial values and expected outcomes satisfying formula fml.

    Synthesize test configurations of both initial values and expected outcomes satisfying formula fml. The values are numeric approximations (avoids Mathematica precision limit issues).

  34. def timeConstrained(cmd: String): String
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  35. def timeConstrained(cmd: MExpr): MExpr
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  36. 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
  37. def toString(): String
    Definition Classes
    AnyRef → Any
  38. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  39. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  40. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from KeYmaeraMathematicaBridge[Either[KExpr, NamedSymbol]]

Inherited from AnyRef

Inherited from Any

Ungrouped