diff --git a/src/main/scala/onera/pmlanalyzer/pml/examples/mySys/MySysExport.scala b/src/main/scala/onera/pmlanalyzer/pml/examples/mySys/MySysExport.scala index ec29883..0b345f1 100644 --- a/src/main/scala/onera/pmlanalyzer/pml/examples/mySys/MySysExport.scala +++ b/src/main/scala/onera/pmlanalyzer/pml/examples/mySys/MySysExport.scala @@ -20,8 +20,8 @@ package onera.pmlanalyzer.pml.examples.mySys import onera.pmlanalyzer.pml.exporters.* import onera.pmlanalyzer.pml.model.utils.Message import onera.pmlanalyzer.pml.operators.* -import onera.pmlanalyzer.views.interference.examples.mySys.{MySysApplicativeTableBasedInterferenceSpecification, MySysPhysicalTableBasedInterferenceSpecification} - +import onera.pmlanalyzer.views.interference.examples.mySys.{MySysInterferenceSpecification, MyProcInterferenceSpecification} +import onera.pmlanalyzer.views.interference.exporters.* /** * Program entry point to export several version of Keystone */ @@ -35,8 +35,8 @@ object MySysExport extends App { object MySys extends MyProcPlatform with MySysLibraryConfiguration with MyProcRoutingConfiguration - with MySysPhysicalTableBasedInterferenceSpecification - with MySysApplicativeTableBasedInterferenceSpecification + with MyProcInterferenceSpecification + with MySysInterferenceSpecification // Export only HW used by SW (explicit) MySys.exportRestrictedHWAndSWGraph() @@ -64,4 +64,5 @@ object MySysExport extends App { // Export the transactions defined by the user MySys.exportUserScenarios() + MySys.exportSemanticsSize() } diff --git a/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysPhysicalTableBasedInterferenceSpecification.scala b/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MyProcInterferenceSpecification.scala similarity index 96% rename from src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysPhysicalTableBasedInterferenceSpecification.scala rename to src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MyProcInterferenceSpecification.scala index de9cac5..50126e6 100644 --- a/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysPhysicalTableBasedInterferenceSpecification.scala +++ b/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MyProcInterferenceSpecification.scala @@ -43,7 +43,7 @@ import onera.pmlanalyzer.views.interference.operators.* * } * }}} */ -trait MySysPhysicalTableBasedInterferenceSpecification extends PhysicalTableBasedInterferenceSpecification { +trait MyProcInterferenceSpecification extends PhysicalTableBasedInterferenceSpecification { self: MyProcPlatform => //Encoding of Rule 1 and Rule 2 diff --git a/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysInterferenceGeneration.scala b/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysInterferenceGeneration.scala new file mode 100644 index 0000000..33fe395 --- /dev/null +++ b/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysInterferenceGeneration.scala @@ -0,0 +1,35 @@ +/******************************************************************************* + * Copyright (c) 2023. ONERA + * This file is part of PML Analyzer + * + * PML Analyzer is free software ; + * you can redistribute it and/or modify it under the terms of the GNU Lesser General Public + * License as published by the Free Software Foundation ; + * either version 2 of the License, or (at your option) any later version. + * + * PML Analyzer is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY ; + * without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + * See the GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License along with this program ; + * if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + ******************************************************************************/ + +package onera.pmlanalyzer.views.interference.examples.mySys + +import onera.pmlanalyzer.pml.examples.mySys.MySysExport.* +import onera.pmlanalyzer.views.interference.operators.* + +import scala.concurrent.duration.* +import scala.language.postfixOps + +/** + * Compute the interference of the SimpleKeystone defined in [[pml.examples.mySys.MySysExport]] + */ +object MySysInterferenceGeneration extends App { + // Compute only up to 2-ite and 2-free + MySys.computeKInterference(2, 2 hours) + + // Compute all ite and itf for benchmarks + MySys.computeAllInterference( 2 hours, ignoreExistingAnalysisFiles = true) +} diff --git a/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysApplicativeTableBasedInterferenceSpecification.scala b/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysInterferenceSpecification.scala similarity index 94% rename from src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysApplicativeTableBasedInterferenceSpecification.scala rename to src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysInterferenceSpecification.scala index 04bd484..a3a5ec7 100644 --- a/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysApplicativeTableBasedInterferenceSpecification.scala +++ b/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/MySysInterferenceSpecification.scala @@ -30,7 +30,7 @@ import onera.pmlanalyzer.views.interference.operators.* * {{{app3 notInterfereWith TeraNet.periph_bus.loads}}} * @see [[views.interference.operators.Exclusive.Ops]] for interfere operator definition */ -trait MySysApplicativeTableBasedInterferenceSpecification extends ApplicativeTableBasedInterferenceSpecification { +trait MySysInterferenceSpecification extends ApplicativeTableBasedInterferenceSpecification { self: MyProcPlatform with MySysTransactionLibrary with MySysLibraryConfiguration with MySysSoftwareAllocation => app22 exclusiveWith app3 diff --git a/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/package.scala b/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/package.scala new file mode 100644 index 0000000..85eef61 --- /dev/null +++ b/src/main/scala/onera/pmlanalyzer/views/interference/examples/mySys/package.scala @@ -0,0 +1,27 @@ +/******************************************************************************* + * Copyright (c) 2023. ONERA + * This file is part of PML Analyzer + * + * PML Analyzer is free software ; + * you can redistribute it and/or modify it under the terms of the GNU Lesser General Public + * License as published by the Free Software Foundation ; + * either version 2 of the License, or (at your option) any later version. + * + * PML Analyzer is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY ; + * without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + * See the GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License along with this program ; + * if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + ******************************************************************************/ + +package onera.pmlanalyzer.views.interference.examples + +/** + * Package containing an example on a simplification of a TI Keystone platform + * @see [[MyProcPhysicalTableBasedInterferenceSpecification]] provides an example of hardware interference assumption modelling + * @see [[MySysInterferenceSpecification]] provides an example of application interference assumption modelling + * @see [[MySysInterferenceGeneration]] provides an example of interference analysis for the simplified + * Keystone platform + */ +package object mySys \ No newline at end of file diff --git a/src/main/scala/onera/pmlanalyzer/views/interference/exporters/InterferenceGraphExporter.scala b/src/main/scala/onera/pmlanalyzer/views/interference/exporters/InterferenceGraphExporter.scala index 2429003..8ce1192 100644 --- a/src/main/scala/onera/pmlanalyzer/views/interference/exporters/InterferenceGraphExporter.scala +++ b/src/main/scala/onera/pmlanalyzer/views/interference/exporters/InterferenceGraphExporter.scala @@ -21,7 +21,7 @@ import onera.pmlanalyzer.pml.exporters.UMLExporter.DOTServiceOnly import onera.pmlanalyzer.pml.exporters.{FileManager, UMLExporter} import onera.pmlanalyzer.pml.model.hardware.Platform import onera.pmlanalyzer.views.interference.model.specification.InterferenceSpecification -import onera.pmlanalyzer.views.interference.model.specification.InterferenceSpecification.{PhysicalScenarioId, scenarioSetId} +import onera.pmlanalyzer.views.interference.model.specification.InterferenceSpecification.{PhysicalScenarioId, multiTransactionId} import java.io.FileWriter @@ -29,9 +29,9 @@ object InterferenceGraphExporter { trait Ops { implicit class InterferenceGraphExporterOps(x: Platform with InterferenceSpecification) extends UMLExporter.Ops { def exportGraph(it: Set[PhysicalScenarioId]): Unit = { - val scenarioSetName = scenarioSetId(it.map(x => PhysicalScenarioId(x.id))) + val multiTransactionName = multiTransactionId(it.map(x => PhysicalScenarioId(x.id))) implicit val writer: FileWriter = new FileWriter(FileManager.exportDirectory.getFile( - s"${x.fullName}_${if(scenarioSetName.id.name.length >= 100) scenarioSetName.hashCode.toString else scenarioSetName}.dot" + s"${x.fullName}_${if(multiTransactionName.id.name.length >= 100) multiTransactionName.hashCode.toString else multiTransactionName}.dot" )) DOTServiceOnly.resetService() DOTServiceOnly.writeHeader diff --git a/src/main/scala/onera/pmlanalyzer/views/interference/exporters/SemanticsExporter.scala b/src/main/scala/onera/pmlanalyzer/views/interference/exporters/SemanticsExporter.scala new file mode 100644 index 0000000..12b1ad3 --- /dev/null +++ b/src/main/scala/onera/pmlanalyzer/views/interference/exporters/SemanticsExporter.scala @@ -0,0 +1,43 @@ +/******************************************************************************* + * Copyright (c) 2023. ONERA + * This file is part of PML Analyzer + * + * PML Analyzer is free software ; + * you can redistribute it and/or modify it under the terms of the GNU Lesser General Public + * License as published by the Free Software Foundation ; + * either version 2 of the License, or (at your option) any later version. + * + * PML Analyzer is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY ; + * without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + * See the GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License along with this program ; + * if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + ******************************************************************************/ + +package onera.pmlanalyzer.views.interference.exporters + +import onera.pmlanalyzer.pml.model.hardware.{Hardware, Platform} +import onera.pmlanalyzer.pml.operators.Provided +import onera.pmlanalyzer.views.interference.operators.* +import onera.pmlanalyzer.pml.exporters.FileManager + +import java.io.{File, FileWriter} + +object SemanticsExporter { + trait Ops { + extension[T<: Platform](self:T) { + def exportSemanticsSize()(using ev: Analyse[T],p:Provided[T,Hardware]): File = { + val file = FileManager.exportDirectory.getFile(self.fullName + "SemanticsSize.txt") + val writer = new FileWriter(file) + val semantics = self.getSemanticsSize + writer.write("Multi-transaction cardinal, Number\n") + for( (i,n) <- semantics) + writer.write(s"$i, $n\n") + writer.close() + file + } + } + } + +} diff --git a/src/main/scala/onera/pmlanalyzer/views/interference/exporters/package.scala b/src/main/scala/onera/pmlanalyzer/views/interference/exporters/package.scala index 86e9c3f..6266ed2 100644 --- a/src/main/scala/onera/pmlanalyzer/views/interference/exporters/package.scala +++ b/src/main/scala/onera/pmlanalyzer/views/interference/exporters/package.scala @@ -27,4 +27,5 @@ package onera.pmlanalyzer.views.interference * Example of usages are provided in ??? */ package object exporters extends IDPExporter.Ops - with InterferenceGraphExporter.Ops + with InterferenceGraphExporter.Ops + with SemanticsExporter.Ops diff --git a/src/main/scala/onera/pmlanalyzer/views/interference/model/specification/InterferenceSpecification.scala b/src/main/scala/onera/pmlanalyzer/views/interference/model/specification/InterferenceSpecification.scala index b27e0b2..ef2ddfb 100644 --- a/src/main/scala/onera/pmlanalyzer/views/interference/model/specification/InterferenceSpecification.scala +++ b/src/main/scala/onera/pmlanalyzer/views/interference/model/specification/InterferenceSpecification.scala @@ -148,7 +148,7 @@ trait InterferenceSpecification * @param t the identifier of the transaction * @return the path of the transaction */ - final def purify(t: PhysicalTransactionId): PhysicalTransaction = transactionsByName.get(t) match { + private final def purify(t: PhysicalTransactionId): PhysicalTransaction = transactionsByName.get(t) match { case Some(h :: tail) => (h +: (transactionInterfereWith(t).toList.sortBy(_.name.name) ++ tail)).filterNot(transactionNotInterfereWith(t)) case _ => Nil @@ -337,18 +337,18 @@ object InterferenceSpecification { case class PhysicalScenarioId(id: Symbol) extends Id - case class PhysicalScenarioSetId(id: Symbol) extends Id + case class PhysicalMultiTransactionId(id: Symbol) extends Id case class ChannelId(id: Symbol) extends Id - def scenarioSetId(t: Iterable[PhysicalScenarioId]): PhysicalScenarioSetId = - PhysicalScenarioSetId(Symbol(t.map(_.id.name).toArray.sorted.mkString("< ", " || ", " >"))) + def multiTransactionId(t: Iterable[PhysicalScenarioId]): PhysicalMultiTransactionId = + PhysicalMultiTransactionId(Symbol(t.map(_.id.name).toArray.sorted.mkString("< ", " || ", " >"))) def channelId(t: Set[Service]): ChannelId = ChannelId(Symbol(t.map(_.toString).toArray.sorted.mkString("{ ", ", ", " }"))) - def groupedScenarioLitId(s: Set[PhysicalScenarioId]): PhysicalScenarioSetId = - PhysicalScenarioSetId(Symbol(scenarioSetId(s).id.name.replace(" ", ""))) + def groupedScenarioLitId(s: Set[PhysicalScenarioId]): PhysicalMultiTransactionId = + PhysicalMultiTransactionId(Symbol(multiTransactionId(s).id.name.replace(" ", ""))) trait Default extends InterferenceSpecification { diff --git a/src/main/scala/onera/pmlanalyzer/views/interference/operators/Analyse.scala b/src/main/scala/onera/pmlanalyzer/views/interference/operators/Analyse.scala index b371717..98fec54 100644 --- a/src/main/scala/onera/pmlanalyzer/views/interference/operators/Analyse.scala +++ b/src/main/scala/onera/pmlanalyzer/views/interference/operators/Analyse.scala @@ -46,7 +46,7 @@ import scala.language.postfixOps * Base trait providing proof that an element is analysable with monosat * @tparam T the type of the component (contravariant) */ -private[operators] trait Analyse[-T] { +trait Analyse[-T] { def computeInterference( x:T, maxSize: Int, @@ -55,6 +55,7 @@ private[operators] trait Analyse[-T] { def printGraph(platform: T): File + def getSemanticsSize(platform: T, max: Int): Map[Int,BigInt] } object Analyse { @@ -131,6 +132,9 @@ object Analyse { verboseResultFile: Boolean = false )(using ev: Analyse[T], p:Provided[T,Hardware]): Set[File] = Await.result(ev.computeInterference(self, self.initiators.size, ignoreExistingAnalysisFiles, verboseResultFile),timeout) + + def getSemanticsSize(using ev: Analyse[T],p:Provided[T,Hardware]) : Map[Int, BigInt]= + ev.getSemanticsSize(self,self.initiators.size) } } @@ -156,14 +160,14 @@ object Analyse { /** - * Sequential version of MONOSAT-based interference computation - * The parallelization is impossible, MONOSAT is tied to a native library so cannot ensure that parallel calls - * are safe (TOO BAD) - * - * @param platform the platform for which the interference are computed, must contained the extra information - * for the interference calculus - * @return the files containing the results of the interference calculus - */ + * Sequential version of MONOSAT-based interference computation + * The parallelization is impossible, MONOSAT is tied to a native library so cannot ensure that parallel calls + * are safe (TOO BAD) + * + * @param platform the platform for which the interference are computed, must contained the extra information + * for the interference calculus + * @return the files containing the results of the interference calculus + */ def computeInterference( platform: ConfiguredPlatform, maxSize: Int, @@ -217,7 +221,7 @@ object Analyse { println(Message.startingNonExclusiveScenarioEstimationInfo(platform.fullName)) val estimateNonExclusiveScenarioStart = System.currentTimeMillis().toFloat - val nonExclusiveScenarios = getNonExclusiveScenarioSetCard(platform, sizes.max) + val nonExclusiveScenarios = getSemanticsSize(platform, sizes.max) println(Message.successfulNonExclusiveScenarioEstimationInfo(platform.fullName, (System.currentTimeMillis().toFloat - estimateNonExclusiveScenarioStart) * 1E-3)) for {(k, v) <- problem.litToNodeSet @@ -230,7 +234,7 @@ object Analyse { println(Message.iterationCompletedInfo(1, sizes.max, (System.currentTimeMillis() - assessmentStartDate) * 1E-3)) - for(size <- sizes) { + for (size <- sizes) { assert(nbITF(size) <= nonExclusiveScenarios(size), s"[ERROR] Interference analysis is unsound, the number of $size-itf is greater thant $size-scenarios") assert(nbFree(size) <= nonExclusiveScenarios(size), s"[ERROR] Interference analysis is unsound, the number of $size-free is greater thant $size-scenarios") } @@ -250,7 +254,7 @@ object Analyse { s.assertTrue(not(monosat.Logic.and(cube.values.toSeq.asJava))) } s.close() - println(Message.iterationCompletedInfo(size,sizes.max, (System.currentTimeMillis() - iterationStartDate) * 1E-3)) + println(Message.iterationCompletedInfo(size, sizes.max, (System.currentTimeMillis() - iterationStartDate) * 1E-3)) if (size == 2) assert(nbITF(2) + nbFree(2) == nonExclusiveScenarios(2), "[ERROR] Interference analysis is unsound, the sum of 2-itf and 2-free is not equal to 2-scenarios") assert(nbITF(size) <= nonExclusiveScenarios(size), s"[ERROR] Interference analysis is unsound, the number of $size-itf is greater thant $size-scenarios") @@ -281,7 +285,7 @@ object Analyse { w.flush() w.close() } - println(Message.analysisCompletedInfo("Interference analysis",computationTime)) + println(Message.analysisCompletedInfo("Interference analysis", computationTime)) files } } @@ -291,14 +295,14 @@ object Analyse { private def nodeId(s: Set[Service]): NodeId = Symbol(s.toList.map(_.toString).sorted.mkString("<", "$", ">")) /** - * Definition of the core problem without cardinality constraints on interference sets - * - * @param platform the platform on which the interference analysis is performed - * @return the variables and constraints to be instantiated in a MONOSAT Solver - */ + * Definition of the core problem without cardinality constraints on interference sets + * + * @param platform the platform on which the interference analysis is performed + * @return the variables and constraints to be instantiated in a MONOSAT Solver + */ private def computeProblemConstraints( - platform: ConfiguredPlatform, - maxSize: Int): Problem = { + platform: ConfiguredPlatform, + maxSize: Int): Problem = { // Utilitarian functions val addNode: Set[Service] => MNode = immutableHashMapMemo { ss => MNode(nodeId(ss)) } @@ -516,7 +520,7 @@ object Analyse { private def updateResultFile(writer: Map[Int, FileWriter], m: Map[Int, Set[Set[UserScenarioId]]]): Unit = { for ((k, v) <- m; ss <- v) - writer(k).write(s"${scenarioSetId(ss.map(s => PhysicalScenarioId(s.id)))}\n") + writer(k).write(s"${multiTransactionId(ss.map(s => PhysicalScenarioId(s.id)))}\n") } private def updateNumber(nbITF: mutable.Map[Int, Int], m: Map[Int, Set[Set[UserScenarioId]]]): Unit = { @@ -542,143 +546,143 @@ object Analyse { channels(k) = v } } - } - - /** - * Compute the number of possible scenario sets for a given platform, this result can be used to estimate - * the proportion of itf or free scenario sets over all possible sets. It can be used to check - * that 2-ift + 2-free = 2-non-exclusive (for higher cardinalities, the estimation of k-redundant is needed) - * - * @param platform the studied platform - * @return the number of scenario sets per size - */ - def getNonExclusiveScenarioSetCard(platform: ConfiguredPlatform, max: Int): Map[Int, BigInt] = platform match { - case app: (ApplicativeTableBasedInterferenceSpecification & TransactionLibrary) => - getNonExclusiveScenarioSetCardApp(app, max) - case _ => - getNonExclusiveScenarioSetCardNoApp(platform, max) - } - def getNonExclusiveScenarioSetCardNoApp(platform: ConfiguredPlatform, max: Int): Map[Int, BigInt] = { - val scenario = platform.purifiedScenarios - val exclusive = platform.finalExclusive(scenario.keySet) - val factory = new SymbolBDDFactory() - val bdd = getNonExclusiveKBDD(scenario.keySet.toSeq, exclusive, max, factory) - - // for each cardinality, compute the number of satisfying assignments of the BDD encoding scenario sets - // containing exactly k non exclusive scenarios - val result = platform match { - case l: TransactionLibrary => - val weightMap = scenario - .transform((_, v) => l.scenarioUserName(v)) - .map(kv => kv._1.id -> kv._2.size) - .filter(_._2 >= 1) - bdd.transform((_, v) => factory.getPathCount(v, weightMap)) + /** + * Compute the number of possible scenario sets for a given platform, this result can be used to estimate + * the proportion of itf or free scenario sets over all possible sets. It can be used to check + * that 2-ift + 2-free = 2-non-exclusive (for higher cardinalities, the estimation of k-redundant is needed) + * + * @param platform the studied platform + * @return the number of scenario sets per size + */ + def getSemanticsSize(platform: ConfiguredPlatform, max: Int): Map[Int, BigInt] = platform match { + case app: (ApplicativeTableBasedInterferenceSpecification & TransactionLibrary) => + getSemanticsSizeWithApp(app, max) case _ => - bdd.transform((_, v) => factory.getPathCount(v)) + getSemanticsSizeWithoutApp(platform, max) } - factory.dispose() - result - } - def getNonExclusiveKBDD[T](values: Seq[T], exclusive: Map[T, Set[T]], max: Int, factory: SymbolBDDFactory): Map[Int, BDD] = { - val symbols = values.map(x => x -> factory.getVar(Symbol(x.toString))).toMap + private def getSemanticsSizeWithoutApp(platform: ConfiguredPlatform, max: Int): Map[Int, BigInt] = { + val scenario = platform.purifiedScenarios + val exclusive = platform.finalExclusive(scenario.keySet) + val factory = new SymbolBDDFactory() + val bdd = getNonExclusiveKBDD(scenario.keySet.toSeq, exclusive, max, factory) + + // for each cardinality, compute the number of satisfying assignments of the BDD encoding scenario sets + // containing exactly k non exclusive scenarios + val result = platform match { + case l: TransactionLibrary => + val weightMap = scenario + .transform((_, v) => l.scenarioUserName(v)) + .map(kv => kv._1.id -> kv._2.size) + .filter(_._2 >= 1) + bdd.transform((_, v) => factory.getPathCount(v, weightMap)) + case _ => + bdd.transform((_, v) => factory.getPathCount(v)) + } + factory.dispose() + result + } - // when a scenario s is selected then at no other scenarios is exclusive with it - // \bigwedge_{s \in scenarioVar} bdd(s) \Rightarrow not \bigvee_{s' \in exclusive(s)} bdd(s') - val isExclusive = factory.andBDD(exclusive.map(p => - symbols(p._1).imp(factory.orBDD(p._2.map(symbols)).not) - )) + private def getNonExclusiveKBDD[T](values: Seq[T], exclusive: Map[T, Set[T]], max: Int, factory: SymbolBDDFactory): Map[Int, BDD] = { + val symbols = values.map(x => x -> factory.getVar(Symbol(x.toString))).toMap - (2 to max).map(k => - k -> factory.mkExactlyK(values.map(x => Symbol(x.toString)), k).and(isExclusive) - ).toMap - } + // when a scenario s is selected then at no other scenarios is exclusive with it + // \bigwedge_{s \in scenarioVar} bdd(s) \Rightarrow not \bigvee_{s' \in exclusive(s)} bdd(s') + val isExclusive = factory.andBDD(exclusive.map(p => + symbols(p._1).imp(factory.orBDD(p._2.map(symbols)).not) + )) - def getNonExclusiveScenarioSetCardApp(platform: ConfiguredLibraryBasedPlatform, max: Int): Map[Int, BigInt] = { - val factory = new SymbolBDDFactory() - val result = getNonExclusiveKBDD( - platform.scenarioByUserName.keys.toSeq, - platform.finalUserScenarioExclusive, - max, - factory).transform((_, v) => factory.getPathCount(v)) - factory.dispose() - result - } + (2 to max).map(k => + k -> factory.mkExactlyK(values.map(x => Symbol(x.toString)), k).and(isExclusive) + ).toMap + } - /** - * Compute the number of k-redundant scenario sets for a given platform, it can be used to check that - * for all size, k-free + k-itf + k-redundant = k-non-exclusive - * - * @param platform the platform to analyse - * @param free the interference free scenario sets - * @param itf the interference scenario sets - * @return the number of k-redundant per size - */ - @deprecated("poor performance computation of k-redundant cardinal since based on a building out of free and itf" + - "results that are classically very large") - def getRedundantCard( - platform: ConfiguredPlatform, - free: Set[Set[PhysicalScenarioId]], - itf: Set[Set[PhysicalScenarioId]]): Map[Int, BigInt] = { - val idToScenario = platform.purifiedScenarios - val exclusive = idToScenario.keySet.groupMapReduce(t => t)(t => idToScenario.keySet.filter(platform.finalExclusive(t, _)))(_ ++ _) - val allResults = free ++ itf - val scenarioToScenarioSet = allResults - .flatMap(ss => ss.map(s => s -> ss)) - .groupMap(_._1)(_._2) - val scenarioVar = idToScenario.keys.toSeq - val nonEmptyChannelResults = platform - .channelNonEmpty(allResults) - val factory = new SymbolBDDFactory() - - - val isNonExclusive = exclusive.foldLeft(factory.one())((acc, p) => acc.and( - factory.getVar(p._1.id).imp( - p._2.foldLeft(factory.zero())((orAcc, s) => orAcc.or(factory.getVar(s.id))).not()) - )) - // if s in scenarioVar is selected then at least one free or itf is selected - val sSelect: BDD = factory.andBDD( - scenarioToScenarioSet.map(p => - factory - .getVar(p._1.id) - .imp(factory.orBDD(p._2.map(ss => - factory.getVar(InterferenceSpecification.scenarioSetId(ss).id)))))) - // if a result is selected then all of its scenarios are selected - val resultSelect: BDD = factory.andBDD( - allResults.map(ss => - factory.getVar(InterferenceSpecification.scenarioSetId(ss).id) - .imp(factory.andBDD(ss.map(s => factory.getVar(s.id)))))) - // if an itf is selected then all itfs owning an interference channel with the itf must be discarded - // i.e. all the itfs sharing a common service with itf or using an exclusive service with itf - val emptyChannel = factory.andBDD(nonEmptyChannelResults.map(p => - factory.getVar(InterferenceSpecification.scenarioSetId(p._1).id).imp( - factory.orBDD(p._2.map(ss => factory.getVar(InterferenceSpecification.scenarioSetId(ss).id))).not() - ) - )) - // the selection must contains at least one interference - val atLeastOneITF: BDD = factory.orBDD(itf - .map(InterferenceSpecification.scenarioSetId) - .map(s => factory.getVar(s.id))) - val staticCst = isNonExclusive - .and(sSelect) - .and(resultSelect) - .and(atLeastOneITF) - .and(emptyChannel) - (2 to platform.initiators.size).map(k => - k -> { - val exactlyK = factory.mkExactlyK(scenarioVar.map(_.id), k) - // the selected itf or free must have a cardinality strictly lower than k - val restrictedITFAndFree: BDD = factory.andBDD( - allResults - .filter(ss => ss.size >= k) - .map(InterferenceSpecification.scenarioSetId) - .map(ss => factory.getVar(ss.id).not)) - factory.getPathCount( - exactlyK - .and(restrictedITFAndFree) - .and(staticCst)) - } - ).toMap + private def getSemanticsSizeWithApp(platform: ConfiguredLibraryBasedPlatform, max: Int): Map[Int, BigInt] = { + val factory = new SymbolBDDFactory() + val result = getNonExclusiveKBDD( + platform.scenarioByUserName.keys.toSeq, + platform.finalUserScenarioExclusive, + max, + factory).transform((_, v) => factory.getPathCount(v)) + factory.dispose() + result + } + + /** + * Compute the number of k-redundant scenario sets for a given platform, it can be used to check that + * for all size, k-free + k-itf + k-redundant = k-non-exclusive + * + * @param platform the platform to analyse + * @param free the interference free scenario sets + * @param itf the interference scenario sets + * @return the number of k-redundant per size + */ + @deprecated("poor performance computation of k-redundant cardinal since based on a building out of free and itf" + + "results that are classically very large") + def getRedundantCard( + platform: ConfiguredPlatform, + free: Set[Set[PhysicalScenarioId]], + itf: Set[Set[PhysicalScenarioId]]): Map[Int, BigInt] = { + val idToScenario = platform.purifiedScenarios + val exclusive = idToScenario.keySet.groupMapReduce(t => t)(t => idToScenario.keySet.filter(platform.finalExclusive(t, _)))(_ ++ _) + val allResults = free ++ itf + val scenarioToMultiTransaction = allResults + .flatMap(ss => ss.map(s => s -> ss)) + .groupMap(_._1)(_._2) + val scenarioVar = idToScenario.keys.toSeq + val nonEmptyChannelResults = platform + .channelNonEmpty(allResults) + val factory = new SymbolBDDFactory() + + + val isNonExclusive = exclusive.foldLeft(factory.one())((acc, p) => acc.and( + factory.getVar(p._1.id).imp( + p._2.foldLeft(factory.zero())((orAcc, s) => orAcc.or(factory.getVar(s.id))).not()) + )) + // if s in scenarioVar is selected then at least one free or itf is selected + val sSelect: BDD = factory.andBDD( + scenarioToMultiTransaction.map(p => + factory + .getVar(p._1.id) + .imp(factory.orBDD(p._2.map(ss => + factory.getVar(InterferenceSpecification.multiTransactionId(ss).id)))))) + // if a result is selected then all of its scenarios are selected + val resultSelect: BDD = factory.andBDD( + allResults.map(ss => + factory.getVar(InterferenceSpecification.multiTransactionId(ss).id) + .imp(factory.andBDD(ss.map(s => factory.getVar(s.id)))))) + // if an itf is selected then all itfs owning an interference channel with the itf must be discarded + // i.e. all the itfs sharing a common service with itf or using an exclusive service with itf + val emptyChannel = factory.andBDD(nonEmptyChannelResults.map(p => + factory.getVar(InterferenceSpecification.multiTransactionId(p._1).id).imp( + factory.orBDD(p._2.map(ss => factory.getVar(InterferenceSpecification.multiTransactionId(ss).id))).not() + ) + )) + // the selection must contains at least one interference + val atLeastOneITF: BDD = factory.orBDD(itf + .map(InterferenceSpecification.multiTransactionId) + .map(s => factory.getVar(s.id))) + val staticCst = isNonExclusive + .and(sSelect) + .and(resultSelect) + .and(atLeastOneITF) + .and(emptyChannel) + (2 to platform.initiators.size).map(k => + k -> { + val exactlyK = factory.mkExactlyK(scenarioVar.map(_.id), k) + // the selected itf or free must have a cardinality strictly lower than k + val restrictedITFAndFree: BDD = factory.andBDD( + allResults + .filter(ss => ss.size >= k) + .map(InterferenceSpecification.multiTransactionId) + .map(ss => factory.getVar(ss.id).not)) + factory.getPathCount( + exactlyK + .and(restrictedITFAndFree) + .and(staticCst)) + } + ).toMap + } } }