class NonInterferenceChecker extends SoftwareInterpolationFramework
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- NonInterferenceChecker
- SoftwareInterpolationFramework
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Instance Constructors
- new NonInterferenceChecker(progCtor: (FrameworkVocabulary) => ConcurrentProgram)
Type Members
- class ModelChecker extends AnyRef
- case class NIAssertion(id1: ConstantTerm, id2: ConstantTerm, globalState: Seq[ConstantTerm], localState1: Seq[ConstantTerm], localState2: Seq[ConstantTerm])(implicit st: SigTracker) extends Product with Serializable
- case class NICheck(inv1: IFormula, inv2: IFormula)(implicit st: SigTracker) extends Product with Serializable
- case class NIInterpolation(inv1: IFormula, inv2: IFormula, path1: Int, path2: Int)(implicit st: SigTracker) extends Product with Serializable
- case class OwickiGriesCheck(inv1: IFormula, inv2: IFormula)(implicit st: SigTracker) extends Product with Serializable
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(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- def dumpInterpolationProblem(transitionParts: Map[PartName, Conjunction], sig: Signature): Unit
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- val frameworkVocabulary: FrameworkVocabulary
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def genInterpolants(formulas: Seq[Conjunction], commonFormula: Conjunction, order: TermOrder): Either[Conjunction, Iterator[Conjunction]]
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def instantiatePreVars(f: IFormula, concreteId: ConstantTerm, lPre: Seq[ConstantTerm], gPre: Seq[ConstantTerm]): IFormula
- var interpolationProblemBasename: String
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- var interpolationProblemNum: Int
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- lazy val interpolationProver: IncProver
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def parseAndSimplify(input: Reader): (Map[PartName, Conjunction], Signature)
Read a given problem, split it into the different parts, try to simplify bitvector expressions as far as possible, and convert it to internal presentation.
Read a given problem, split it into the different parts, try to simplify bitvector expressions as far as possible, and convert it to internal presentation. Bitvector simplifications are done based on the type declarations inSigned, inUnsigned, and inArray. The problem will also be restructured such that the type declaration of a constant occurs in the first part in which the constant is used (sorted the partitions lexicographically according to their name).
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def parseProblem(reader: Reader): (IFormula, Signature)
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- val preludeSignature: Signature
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- val program: ConcurrentProgram
- def simplifyBitvectorFor(f: IFormula, typeAssumptions: IFormula): IFormula
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def sortNamesLex[A](transitionParts: Map[PartName, A]): Seq[PartName]
Sort the transition relations lexicographically according to their name; NO_NAME is ignored and removed
Sort the transition relations lexicographically according to their name; NO_NAME is ignored and removed
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toInputAbsyAndSimplify(c: Conjunction): IFormula
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def toInternal(f: IFormula, sig: Signature): (Conjunction, TermOrder)
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def toNamedParts(f: IFormula, sig: Signature): (Map[PartName, Conjunction], Signature)
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def toString(): String
- Definition Classes
- AnyRef → Any
- lazy val validityCheckProver: IncProver
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- object InterferenceException extends Exception
- object OwickiGriesException extends Exception
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)