pml_analyzer
DocsAPI
Generated with
pml_analyzer/onera.pmlanalyzer.views.interference.model.formalisation

onera.pmlanalyzer.views.interference.model.formalisation

package onera.pmlanalyzer.views.interference.model.formalisation

Package containing model extension enabling formalisation of the interference computation problem as an SMT problem.

Attributes

See also:

BDDFactory provides some basic Binary Decision Diagram features based on JavaBDD.

ProblemElement provides all the necessary modelling features to encode the problem with Monosat

Members list

Concise view

Type members

Classlikes

trait ALit extends ProblemElement

Attributes

Graph
Supertypes
class Object
trait Matchable
class Any
Known subtypes
class And
class Equal
class Implies
class MEdgeLit
class MLit
class Not
class Or
class Reaches
case class And(l: ALit*) extends ALit

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait ALit
class Object
trait Matchable
class Any
trait Assert extends ProblemElement

Attributes

Graph
Supertypes
class Object
trait Matchable
class Any
Known subtypes
class AssertPB
case class AssertPB(l: Set[ALit], comp: Comparison, k: Int) extends Assert

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait Assert
class Object
trait Matchable
class Any
class BDDFactory extends BaseBDDFactory[Int, BDD]

Class for a classic BDD Factory (variable are integer and BDD are JavaBDD)

Class for a classic BDD Factory (variable are integer and BDD are JavaBDD)

Attributes

Graph
Supertypes
trait BaseBDDFactory[Int, BDD]
class Object
trait Matchable
class Any
trait BaseBDDFactory[Var, MyBDD <: BDD]

base trait for BDD factories

base trait for BDD factories

Attributes

MyBDD

the BDD representation which must be a subtype of JavaBDD type

Var

the type of variable labelled on BDD nodes

Graph
Supertypes
class Object
trait Matchable
class Any
Known subtypes
trait GenBDDFactory[Var]
case class Equal(l: ALit, r: ALit) extends ALit

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait ALit
class Object
trait Matchable
class Any
trait GenBDDFactory[Var] extends BaseBDDFactory[Var, BDD]

Generic BDD factory over the type of BDD variables

Generic BDD factory over the type of BDD variables

Attributes

Var

the type of variable labelled on BDD nodes

Graph
Supertypes
trait BaseBDDFactory[Var, BDD]
class Object
trait Matchable
class Any
Known subtypes
case class Implies(l: ALit, r: ALit) extends ALit

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait ALit
class Object
trait Matchable
class Any
case class MEdge(from: MNode, to: MNode, id: EdgeId) extends ProblemElement

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
case class MEdgeLit(edge: MEdge, graph: MGraph) extends ALit

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait ALit
class Object
trait Matchable
class Any
case class MGraph(nodes: Set[MNode], edges: Set[MEdge]) extends ProblemElement

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
case class MLit(id: LitId) extends ALit

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait ALit
class Object
trait Matchable
class Any
case class MNode(id: NodeId) extends ProblemElement

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
case class Not(l: ALit) extends ALit

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait ALit
class Object
trait Matchable
class Any
case class Or(l: ALit*) extends ALit

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait ALit
class Object
trait Matchable
class Any
class Problem(val platform: Platform & InterferenceSpecification, val groupedScenarios: Map[MLit, Set[PhysicalScenarioId]], val litToNodeSet: Map[MLit, Set[Set[MNode]]], val idToScenario: Map[PhysicalScenarioId, PhysicalScenario], val exclusiveScenarios: Map[PhysicalScenarioId, Set[PhysicalScenarioId]], val serviceGraph: MGraph, val isFree: ALit, val isITF: ALit, val pbCst: Set[AssertPB], val simpleCst: Set[SimpleAssert], val nodeToServices: Map[MNode, Set[Service]], val serviceToScenarioLit: Map[Service, Set[PhysicalScenarioId]], val maxSize: Option[Int]) extends ProblemElement

Attributes

Companion:
object
Graph
Supertypes
class Object
trait Matchable
class Any
object Problem

Attributes

Companion:
class
Graph
Supertypes
class Object
trait Matchable
class Any
Self type
Problem.type
trait ProblemElement

Attributes

Companion:
object
Graph
Supertypes
class Object
trait Matchable
class Any
Known subtypes
trait ALit
class And
class Equal
class Implies
class MEdgeLit
class MLit
class Not
class Or
class Reaches
trait Assert
class AssertPB
class MEdge
class MGraph
class MNode
class Problem
object ProblemElement

Attributes

Companion:
trait
Graph
Supertypes
class Object
trait Matchable
class Any
Self type
case class Reaches(graph: MGraph, from: MNode, to: MNode) extends ALit

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait ALit
class Object
trait Matchable
class Any
case class SimpleAssert(l: ALit) extends Assert

Attributes

Graph
Supertypes
trait Serializable
trait Product
trait Equals
trait Assert
class Object
trait Matchable
class Any
class SymbolBDDFactory extends GenBDDFactory[Symbol]

BDDFactory where variables labelled on BDD node are InstBoolIdent

BDDFactory where variables labelled on BDD node are InstBoolIdent

Attributes

Graph
Supertypes
trait GenBDDFactory[Symbol]
trait BaseBDDFactory[Symbol, BDD]
class Object
trait Matchable
class Any
Generated with