Packages

o

edu.cmu.cs.ls.keymaerax.hydra

DatabasePopulator

object DatabasePopulator extends Logging

Populates the database from a JSON collection of models and tactics.

Linear Supertypes
Logging, LazyLogging, LoggerHolder, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. DatabasePopulator
  2. Logging
  3. LazyLogging
  4. LoggerHolder
  5. AnyRef
  6. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class ImportResult(succeeded: List[(String, Int)], failed: List[String]) extends Product with Serializable

    Succeeded imports: model name and created Id, failed: model name.

  2. case class TutorialEntry(name: String, model: String, description: Option[String], title: Option[String], link: Option[String], tactic: List[(String, String, Boolean)], kind: String = "Unknown") extends Product with Serializable

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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  6. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  7. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  8. def executeTactic(db: DBAbstraction, model: String, proofId: Int, tactic: String): Unit

    Executes the tactic on the model and records the tactic steps as proof in the database.

  9. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  10. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  11. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def importKya(db: DBAbstraction, user: String, url: String, prove: Boolean, exclude: List[ModelPOJO]): ImportResult

    Imports an archive from URL.

    Imports an archive from URL. Optionally proves the models when tactics are present.

  13. def importModel(db: DBAbstraction, user: String, prove: Boolean)(entry: TutorialEntry): Either[(String, Int), String]

    Imports a model with info into the database; optionally records a proof obtained using tactic.

    Imports a model with info into the database; optionally records a proof obtained using tactic. Returns Left(modelName, ID) on success, Right(modelName) on failure

  14. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  15. def loadResource(url: String): String

    Loads the specified resource, either from the JAR if URL starts with 'classpath:' or from the URL.

    Loads the specified resource, either from the JAR if URL starts with 'classpath:' or from the URL.

    Annotations
    @tailrec()
  16. lazy val logger: Logger
    Attributes
    protected
    Definition Classes
    LazyLogging → LoggerHolder
  17. final val loggerName: String
    Attributes
    protected
    Definition Classes
    LoggerHolder
  18. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  20. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. def prepareInterpreter(db: DBAbstraction, proofId: Int, defs: Declaration, listeners: Seq[IOListener] = Nil): Interpreter

    Prepares an interpreter for executing tactics.

  22. def readKyx(url: String): List[TutorialEntry]

    Reads a .kyx archive from the URL url as tutorial entries (i.e., one tactic per entry).

  23. def readTutorialEntries(url: String): List[TutorialEntry]

    Reads tutorial entries from the specified URL.

  24. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  25. def toString(): String
    Definition Classes
    AnyRef → Any
  26. def toTutorialEntry(entry: ParsedArchiveEntry): TutorialEntry

    Converts a parsed archive entry into a tutorial entry as expected by this importer.

  27. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  28. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  29. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Logging

Inherited from LazyLogging

Inherited from LoggerHolder

Inherited from AnyRef

Inherited from Any

Ungrouped