From 4acd3f4c3814cccf18c7063243e58ad0f81c368a Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Sun, 17 Oct 2021 21:50:37 +0300
Subject: [PATCH 01/32] Implement input vars decomposition

---
 .../cli/command/infer/AbstractInferCommand.kt |  1 +
 .../cli/command/infer/options/ExtraOptions.kt | 10 +++
 .../ru/ifmo/fbsat/core/automaton/Automaton.kt | 52 +++++++++----
 .../automaton/ParallelModularAutomaton.kt     | 78 +++++++++++++++----
 .../core/automaton/guard/ConjunctiveGuard.kt  | 43 ++++++++++
 .../AutomatonStructureConstraints.kt          | 38 +++++++++
 .../ru/ifmo/fbsat/core/task/Optimization.kt   | 44 +++++++++++
 .../basic/parallel/ParallelModularBasic.kt    |  8 +-
 .../parallel/ParallelModularBasicVariables.kt | 20 +++++
 .../fbsat/core/task/single/basic/Basic.kt     |  7 +-
 .../core/task/single/basic/BasicVariables.kt  | 35 +++++----
 .../ru/ifmo/fbsat/core/utils/Globals.kt       |  1 +
 12 files changed, 291 insertions(+), 46 deletions(-)
 create mode 100644 fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt

diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
index c046cc79..6bea7866 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
@@ -42,6 +42,7 @@ abstract class AbstractInferCommand<AutomatonType : Any>(name: String) : CliktCo
             Globals.IS_ENCODE_TRANSITION_FUNCTION = isEncodeTransitionFunction
             Globals.IS_ENCODE_EPSILON_PASSIVE = isEncodeEpsilonPassive
             Globals.IS_ENCODE_NOT_EPSILON_ACTIVE = isEncodeNotEpsilonActive
+            Globals.IS_ENCODE_CONJUNCTIVE_GUARDS = isEncodeConjunctiveGuards
             Globals.IS_FIX_ACTIVE = isFixActive
             Globals.IS_REUSE_K = isReuseK
             Globals.IS_USE_ASSUMPTIONS = isUseAssumptions
diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
index 3ea3ab38..6b903240 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
@@ -38,6 +38,7 @@ class ExtraOptions : OptionGroup(EXTRA_OPTIONS) {
     val isEncodeTransitionFunction: Boolean by isEncodeTransitionFunctionOption()
     val isEncodeEpsilonPassive: Boolean by isEncodeEpsilonPassiveOption()
     val isEncodeNotEpsilonActive: Boolean by isEncodeNotEpsilonActiveOption()
+    val isEncodeConjunctiveGuards: Boolean by isEncodeConjunctiveGuardsOption()
     val isFixActive: Boolean by isFixActiveOption()
     val isReuseK: Boolean by isReuseKOption()
     val isUseAssumptions: Boolean by isUseAssumptionsOption()
@@ -244,6 +245,15 @@ fun ParameterHolder.isEncodeNotEpsilonActiveOption() =
         default = Globals.IS_ENCODE_NOT_EPSILON_ACTIVE
     )
 
+fun ParameterHolder.isEncodeConjunctiveGuardsOption() =
+    option(
+        "--encode-conjunctive-guards",
+        help = "Encode conjunctive guards"
+    ).flag(
+        "--no-encode-conjunctive-guards",
+        default = Globals.IS_ENCODE_CONJUNCTIVE_GUARDS
+    )
+
 fun ParameterHolder.isFixActiveOption() =
     option(
         "--fix-active",
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
index 142cffed..9192996a 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
@@ -11,6 +11,7 @@ import com.soywiz.klock.DateTime
 import kotlinx.serialization.Serializable
 import org.redundent.kotlin.xml.xml
 import ru.ifmo.fbsat.core.automaton.guard.BooleanExpressionGuard
+import ru.ifmo.fbsat.core.automaton.guard.ConjunctiveGuard
 import ru.ifmo.fbsat.core.automaton.guard.Guard
 import ru.ifmo.fbsat.core.automaton.guard.NodeType
 import ru.ifmo.fbsat.core.automaton.guard.TruthTableGuard
@@ -330,7 +331,7 @@ class Automaton(
         out@ for ((i, result) in eval(scenario).withIndex()) {
             val element = scenario.elements[i]
             if (result.outputAction != element.outputAction) {
-                // logger.error("No mapping for ${i + 1}-th element = $element, result = $result")
+                logger.error("No mapping for ${i + 1}-th element = $element, result = $result")
                 break@out
             }
             mapping[i] = result
@@ -526,11 +527,12 @@ class Automaton(
 
     fun getStats(): String {
         return "" +
-            "C = $numberOfStates, " +
-            "K = $maxOutgoingTransitions, " +
-            "P = $maxGuardSize, " +
-            "T = $numberOfTransitions, " +
-            "N = $totalGuardsSize"
+            "C = $numberOfStates" +
+            ", K = $maxOutgoingTransitions" +
+            ", P = $maxGuardSize" +
+            ", T = $numberOfTransitions" +
+            ", N = $totalGuardsSize" +
+            ", A = ${transitions.sumOf { (it.guard as? ConjunctiveGuard)?.literals?.size ?: 0 }}"
     }
 
     fun printStats() {
@@ -834,6 +836,7 @@ fun buildBasicAutomaton(
     val scenarioTree: PositiveScenarioTree = context["scenarioTree"]
     val C: Int = context["C"]
     val K: Int = context["K"]
+    val X: Int = context["X"]
     val Z: Int = context["Z"]
     val transitionDestination = context.convertIntVarArray("transitionDestination", model)
     val transitionInputEvent = context.convertIntVarArray("transitionInputEvent", model)
@@ -851,6 +854,14 @@ fun buildBasicAutomaton(
             { true }
         }
 
+    // Only available if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS)
+    val inputVariableUsed by lazy {
+        context.convertBoolVarArray("inputVariableUsed", model)
+    }
+    val inputVariableLiteral by lazy {
+        context.convertBoolVarArray("inputVariableLiteral", model)
+    }
+
     return Automaton(
         scenarioTree = scenarioTree,
         initialOutputValues = initialOutputValues
@@ -875,15 +886,26 @@ fun buildBasicAutomaton(
             scenarioTree.inputEvents[transitionInputEvent[c, k] - 1]
         },
         transitionGuard = { c, k ->
-            TruthTableGuard(
-                truthTable = scenarioTree.uniqueInputs
-                    .withIndex(start = 1)
-                    .associate { (u, input) ->
-                        input to transitionTruthTable[c, k, u]
-                    }
-                // inputNames = scenarioTree.inputNames,
-                // uniqueInputs = scenarioTree.uniqueInputs
-            )
+            if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
+                // inputVariableUsed!!
+                // inputVariableLiteral!!
+                ConjunctiveGuard(
+                    literals = (1..X)
+                        .filter { x -> inputVariableUsed[x] }
+                        .map { x -> if (inputVariableLiteral[c, k, x]) x else -x },
+                    inputNames = scenarioTree.inputNames
+                )
+            } else {
+                TruthTableGuard(
+                    truthTable = scenarioTree.uniqueInputs
+                        .withIndex(start = 1)
+                        .associate { (u, input) ->
+                            input to transitionTruthTable[c, k, u]
+                        }
+                    // inputNames = scenarioTree.inputNames,
+                    // uniqueInputs = scenarioTree.uniqueInputs
+                )
+            }
         }
     )
 }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
index 7ee6bd27..2eaed759 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
@@ -11,6 +11,7 @@ import com.github.lipen.satlib.core.Model
 import com.soywiz.klock.DateTime
 import org.redundent.kotlin.xml.xml
 import ru.ifmo.fbsat.core.automaton.guard.BooleanExpressionGuard
+import ru.ifmo.fbsat.core.automaton.guard.ConjunctiveGuard
 import ru.ifmo.fbsat.core.automaton.guard.NodeType
 import ru.ifmo.fbsat.core.automaton.guard.TruthTableGuard
 import ru.ifmo.fbsat.core.scenario.InputEvent
@@ -153,11 +154,40 @@ class ParallelModularAutomaton(
 
     fun getStats(): String {
         return "M = $numberOfModules, " +
-            "C = ${modules.values.joinToString("+") { it.numberOfStates.toString() }} = $numberOfStates, " +
-            "K = ${modules.values.map { it.maxOutgoingTransitions }}, " +
-            "P = ${modules.values.map { it.maxGuardSize }}, " +
-            "T = ${modules.values.joinToString("+") { it.numberOfTransitions.toString() }} = $numberOfTransitions, " +
-            "N = ${modules.values.joinToString("+") { it.totalGuardsSize.toString() }} = $totalGuardsSize"
+            ", C = ${
+                modules.values.joinToString("+") {
+                    it.numberOfStates.toString()
+                }
+            } = $numberOfStates" +
+            ", K = ${
+                modules.values.map { it.maxOutgoingTransitions }
+            }" +
+            ", P = ${
+                modules.values.map { it.maxGuardSize }
+            }" +
+            ", T = ${
+                modules.values.joinToString("+") {
+                    it.numberOfTransitions.toString()
+                }
+            } = $numberOfTransitions" +
+            ", N = ${
+                modules.values.joinToString("+") {
+                    it.totalGuardsSize.toString()
+                }
+            } = $totalGuardsSize" +
+            ", A = ${
+                modules.values.joinToString("+") {
+                    it.transitions.sumOf {
+                        (it.guard as? ConjunctiveGuard)?.literals?.size ?: 0
+                    }.toString()
+                }
+            } = ${
+                modules.values.sumOf {
+                    it.transitions.sumOf {
+                        (it.guard as? ConjunctiveGuard)?.literals?.size ?: 0
+                    }
+                }
+            }"
     }
 
     fun printStats() {
@@ -312,6 +342,7 @@ fun buildBasicParallelModularAutomaton(
     val modules = modularContext.mapIndexed { (m), ctx ->
         val C: Int = ctx["C"]
         val K: Int = ctx["K"]
+        val X: Int = ctx["X"]
         val Z: Int = ctx["Z"]
         val transitionDestination = ctx.convertIntVarArray("transitionDestination", model)
         val transitionInputEvent = ctx.convertIntVarArray("transitionInputEvent", model)
@@ -322,6 +353,14 @@ fun buildBasicParallelModularAutomaton(
         val moduleOutputVariables = (1..Z).filter { z -> moduleControllingOutputVariable[z] == m }
         val initialOutputValues: OutputValues = ctx["initialOutputValues"]
 
+        // Only available if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS)
+        val inputVariableUsed by lazy {
+            ctx.convertBoolVarArray("inputVariableUsed", model)
+        }
+        val inputVariableLiteral by lazy {
+            ctx.convertBoolVarArray("inputVariableLiteral", model)
+        }
+
         Automaton(
             inputEvents = scenarioTree.inputEvents,
             outputEvents = scenarioTree.outputEvents,
@@ -349,15 +388,26 @@ fun buildBasicParallelModularAutomaton(
                 scenarioTree.inputEvents[transitionInputEvent[c, k] - 1]
             },
             transitionGuard = { c, k ->
-                TruthTableGuard(
-                    truthTable = scenarioTree.uniqueInputs
-                        .withIndex(start = 1)
-                        .associate { (u, input) ->
-                            input to transitionTruthTable[c, k, u]
-                        }
-                    // inputNames = scenarioTree.inputNames,
-                    // uniqueInputs = scenarioTree.uniqueInputs
-                )
+                if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
+                    // inputVariableUsed!!
+                    // inputVariableLiteral!!
+                    ConjunctiveGuard(
+                        literals = (1..X)
+                            .filter { x -> inputVariableUsed[x] }
+                            .map { x -> if (inputVariableLiteral[c, k, x]) x else -x },
+                        inputNames = scenarioTree.inputNames
+                    )
+                } else {
+                    TruthTableGuard(
+                        truthTable = scenarioTree.uniqueInputs
+                            .withIndex(start = 1)
+                            .associate { (u, input) ->
+                                input to transitionTruthTable[c, k, u]
+                            }
+                        // inputNames = scenarioTree.inputNames,
+                        // uniqueInputs = scenarioTree.uniqueInputs
+                    )
+                }
             }
         )
     }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt
new file mode 100644
index 00000000..3dbc67f9
--- /dev/null
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt
@@ -0,0 +1,43 @@
+package ru.ifmo.fbsat.core.automaton.guard
+
+import ru.ifmo.fbsat.core.scenario.InputValues
+import ru.ifmo.fbsat.core.utils.pow
+import ru.ifmo.fbsat.core.utils.toBinaryString
+import ru.ifmo.fbsat.core.utils.toBooleanList
+import kotlin.math.absoluteValue
+
+class ConjunctiveGuard(
+    val literals: List<Int>, // signed 1-based
+    val inputNames: List<String>,
+) : Guard {
+    override val size: Int = literals.size + 1
+
+    override fun eval(inputValues: InputValues): Boolean {
+        return literals.all { lit ->
+            inputValues[lit.absoluteValue - 1] xor (lit < 0)
+        }
+    }
+
+    override fun toSimpleString(): String {
+        return literals.joinToString(" & ") { lit ->
+            (if (lit < 0) "~" else "") + inputNames[lit.absoluteValue - 1]
+        }
+    }
+
+    override fun toGraphvizString(): String {
+        return toSimpleString()
+    }
+
+    override fun toFbtString(): String {
+        return toSimpleString().replace("~", "NOT ").replace(" & ", " AND ")
+    }
+
+    override fun toSmvString(): String {
+        return toSimpleString().replace("~", "!")
+    }
+
+    override fun truthTableString(inputNames: List<String>): String =
+        (0 until 2.pow(inputNames.size)).map { i ->
+            eval(InputValues(i.toString(2).padStart(inputNames.size, '0').toBooleanList()))
+        }.toBinaryString()
+}
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index bdc9af71..265e0cc8 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -6,16 +6,20 @@ import com.github.lipen.satlib.core.BoolVarArray
 import com.github.lipen.satlib.core.IntVarArray
 import com.github.lipen.satlib.core.eq
 import com.github.lipen.satlib.core.neq
+import com.github.lipen.satlib.core.sign
 import com.github.lipen.satlib.op.atLeastOne
 import com.github.lipen.satlib.op.atMostOne
 import com.github.lipen.satlib.op.exactlyOne
 import com.github.lipen.satlib.op.iff
 import com.github.lipen.satlib.op.iffAnd
+import com.github.lipen.satlib.op.iffImply
 import com.github.lipen.satlib.op.imply
 import com.github.lipen.satlib.op.implyAnd
 import com.github.lipen.satlib.op.implyOr
 import com.github.lipen.satlib.solver.Solver
+import ru.ifmo.fbsat.core.scenario.InputValues
 import ru.ifmo.fbsat.core.scenario.OutputValues
+import ru.ifmo.fbsat.core.scenario.ScenarioTree
 import ru.ifmo.fbsat.core.solver.autoneg
 import ru.ifmo.fbsat.core.solver.clause
 import ru.ifmo.fbsat.core.solver.forEachModularContext
@@ -439,4 +443,38 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs(
                             yield(transitionFiring[c, k, e, u])
                     }
     }
+
+    if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
+        val tree: ScenarioTree<*, *> = context["tree"]
+        val uniqueInputs: List<InputValues> = tree.uniqueInputs
+        val X: Int = context["X"]
+        val inputVariableUsed: BoolVarArray = context["inputVariableUsed"]
+        val inputVariableLiteral: BoolVarArray = context["inputVariableLiteral"]
+
+        comment("Conjunctive guards")
+        // tt[c,k,u] <=> AND_{x}(used[x] => (lit[c,k,x] <=> u[x])
+        for (c in 1..C)
+            for (k in 1..K)
+                for (u in Us)
+                    iffAnd(transitionTruthTable[c, k, u]) {
+                        for (x in 1..X) {
+                            val aux = newLiteral()
+                            iffImply(
+                                aux,
+                                inputVariableUsed[x],
+                                inputVariableLiteral[c, k, x] sign uniqueInputs[u - 1][x - 1]
+                            )
+                            yield(aux)
+                        }
+                    }
+
+        // ~used[x] => ~lit[c,k,x]
+        for (c in 1..C)
+            for (k in 1..K)
+                for (x in 1..X)
+                    imply(
+                        -inputVariableUsed[x],
+                        -inputVariableLiteral[c, k, x]
+                    )
+    }
 }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt
index eb14ed2c..2e37253b 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt
@@ -7,6 +7,7 @@ import ru.ifmo.fbsat.core.automaton.Automaton
 import ru.ifmo.fbsat.core.automaton.ConsecutiveModularAutomaton
 import ru.ifmo.fbsat.core.automaton.DistributedAutomaton
 import ru.ifmo.fbsat.core.automaton.ParallelModularAutomaton
+import ru.ifmo.fbsat.core.automaton.guard.ConjunctiveGuard
 import ru.ifmo.fbsat.core.task.distributed.basic.inferDistributedBasic
 import ru.ifmo.fbsat.core.task.distributed.complete.inferDistributedComplete
 import ru.ifmo.fbsat.core.task.distributed.extended.inferDistributedExtended
@@ -114,6 +115,27 @@ fun Inferrer.optimizeN(
     )
 }
 
+@Suppress("FunctionName")
+fun Inferrer.optimizeA(
+    start: Int? = null,
+    end: Int = 0,
+    useAssumptions: Boolean = Globals.IS_USE_ASSUMPTIONS,
+): Automaton? {
+    logger.info("Optimizing A (${if (useAssumptions) "with" else "without"} assumptions) from $start to $end...")
+    val cardinality: Cardinality = solver.context["cardinalityA"]
+    return cardinality.optimizeTopDown(
+        start = start,
+        end = end,
+        useAssumptions = useAssumptions,
+        infer = { inferBasic() },
+        query = {
+            it.transitions.sumOf { t ->
+                (t.guard as ConjunctiveGuard).literals.size
+            }
+        }
+    )
+}
+
 @Suppress("FunctionName")
 fun Inferrer.optimizeN_Forest(
     start: Int? = null,
@@ -244,6 +266,28 @@ fun Inferrer.optimizeArbitraryModularN(
     )
 }
 
+fun Inferrer.optimizeParallelModularA(
+    start: Int? = null,
+    end: Int = 0,
+    useAssumptions: Boolean = Globals.IS_USE_ASSUMPTIONS,
+): ParallelModularAutomaton? {
+    logger.info("Optimizing A (${if (useAssumptions) "with" else "without"} assumptions) from $start to $end...")
+    val cardinality: Cardinality = solver.context["cardinalityA"]
+    return cardinality.optimizeTopDown(
+        start = start,
+        end = end,
+        useAssumptions = useAssumptions,
+        infer = { inferParallelModularBasic() },
+        query = {
+            it.modules.values.sumOf { module ->
+                module.transitions.sumOf { t ->
+                    (t.guard as ConjunctiveGuard).literals.size
+                }
+            }
+        }
+    )
+}
+
 fun Inferrer.optimizeDistributedSumC(
     start: Int? = null,
     end: Int = 0,
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
index 982d333e..9e410cd8 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
@@ -5,7 +5,9 @@ import ru.ifmo.fbsat.core.automaton.ParallelModularAutomaton
 import ru.ifmo.fbsat.core.automaton.buildBasicParallelModularAutomaton
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
 import ru.ifmo.fbsat.core.task.Inferrer
+import ru.ifmo.fbsat.core.task.optimizeParallelModularA
 import ru.ifmo.fbsat.core.task.optimizeParallelModularT
+import ru.ifmo.fbsat.core.utils.Globals
 import ru.ifmo.fbsat.core.utils.MyLogger
 
 private val logger = MyLogger {}
@@ -65,7 +67,11 @@ fun Inferrer.parallelModularBasicMin(
     numberOfStates: Int? = null, // C_start, 1 if null
 ): ParallelModularAutomaton? {
     parallelModularBasicMinC(scenarioTree, numberOfModules = numberOfModules, start = numberOfStates ?: 1)
-    return optimizeParallelModularT()
+    return if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
+        optimizeParallelModularA()
+    } else {
+        optimizeParallelModularT()
+    }
 }
 
 fun Inferrer.inferParallelModularBasic(): ParallelModularAutomaton? {
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
index 1faacacd..4e794b3d 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
@@ -1,6 +1,7 @@
 package ru.ifmo.fbsat.core.task.modular.basic.parallel
 
 import com.github.lipen.satlib.card.declareCardinality
+import com.github.lipen.satlib.core.BoolVarArray
 import com.github.lipen.satlib.core.IntVarArray
 import com.github.lipen.satlib.core.neq
 import com.github.lipen.satlib.core.newIntVarArray
@@ -9,6 +10,7 @@ import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
 import ru.ifmo.fbsat.core.solver.declareModularContext
 import ru.ifmo.fbsat.core.solver.forEachModularContext
 import ru.ifmo.fbsat.core.task.single.basic.declareBasicVariables
+import ru.ifmo.fbsat.core.utils.Globals
 
 @Suppress("LocalVariableName")
 fun Solver.declareParallelModularBasicVariables(
@@ -66,4 +68,22 @@ fun Solver.declareParallelModularBasicVariables(
             }
         }
     }
+    if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
+        comment("Cardinality (A)")
+        val cardinalityA = context("cardinalityA") {
+            declareCardinality {
+                @Suppress("NAME_SHADOWING")
+                forEachModularContext {
+                    val C: Int = context["C"]
+                    val K: Int = context["K"]
+                    val X: Int = context["X"]
+                    val inputVariableUsed: BoolVarArray = context["inputVariableUsed"]
+                    for (c in 1..C)
+                        for (k in 1..K)
+                            for (x in 1..X)
+                                yield(inputVariableUsed[x])
+                }
+            }
+        }
+    }
 }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt
index e7c26e8c..db485342 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt
@@ -10,6 +10,7 @@ import ru.ifmo.fbsat.core.solver.numberOfConflicts
 import ru.ifmo.fbsat.core.solver.numberOfDecisions
 import ru.ifmo.fbsat.core.solver.numberOfPropagations
 import ru.ifmo.fbsat.core.task.Inferrer
+import ru.ifmo.fbsat.core.task.optimizeA
 import ru.ifmo.fbsat.core.task.optimizeT
 import ru.ifmo.fbsat.core.utils.Globals
 import ru.ifmo.fbsat.core.utils.MyLogger
@@ -101,7 +102,11 @@ fun Inferrer.basicMin(
             end = end,
             isEncodeReverseImplication = isEncodeReverseImplication
         ) ?: return@run null
-        optimizeT()
+        if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
+            optimizeA()
+        } else {
+            optimizeT()
+        }
     }
     logger.info("Task basic-min done in %.2f s".format(timeSince(timeStart).seconds))
     if (solver.isSupportStats()) {
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
index a3f1ce59..f8e36616 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
@@ -1,6 +1,7 @@
 package ru.ifmo.fbsat.core.task.single.basic
 
 import com.github.lipen.satlib.card.declareCardinality
+import com.github.lipen.satlib.core.BoolVarArray
 import com.github.lipen.satlib.core.IntVarArray
 import com.github.lipen.satlib.core.eq
 import com.github.lipen.satlib.core.neq
@@ -10,7 +11,6 @@ import com.github.lipen.satlib.core.newIntVarArray
 import com.github.lipen.satlib.solver.Solver
 import ru.ifmo.fbsat.core.scenario.initialOutputValues
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
-import ru.ifmo.fbsat.core.solver.literals
 import ru.ifmo.fbsat.core.utils.Globals
 
 @Suppress("LocalVariableName")
@@ -98,6 +98,14 @@ fun Solver.declareBasicVariables(
     val stateAlgorithmTop = context("stateAlgorithmTop") {
         newBoolVarArray(C, Z)
     }
+    if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
+        val inputVariableUsed = context("inputVariableUsed") {
+            newBoolVarArray(X)
+        }
+        val inputVariableLiteral = context("inputVariableLiteral") {
+            newBoolVarArray(C, K, X)
+        }
+    }
 
     /* Mapping variables */
     comment("Mapping variables")
@@ -119,19 +127,16 @@ fun Solver.declareBasicVariables(
                     yield(transitionDestination[c, k] neq 0)
         }
     }
-
-    if (Globals.IS_DUMP_VARS_IN_CNF) {
-        comment("actualTransitionFunction = ${actualTransitionFunction.literals}")
-        comment("transitionDestination = ${transitionDestination.literals}")
-        comment("transitionInputEvent = ${transitionInputEvent.literals}")
-        comment("transitionTruthTable = ${transitionTruthTable.literals}")
-        comment("transitionFiring = ${transitionFiring.literals}")
-        comment("firstFired = ${firstFired.literals}")
-        comment("notFired = ${notFired.literals}")
-        comment("stateOutputEvent = ${stateOutputEvent.literals}")
-        comment("stateAlgorithmBot = ${stateAlgorithmBot.literals}")
-        comment("stateAlgorithmTop = ${stateAlgorithmTop.literals}")
-        comment("mapping = ${mapping.literals}")
-        comment("totalizerT = ${cardinalityT.totalizer}")
+    if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
+        comment("Cardinality (A)")
+        val inputVariableUsed: BoolVarArray = context["inputVariableUsed"]
+        val cardinalityA = context("cardinalityA") {
+            declareCardinality {
+                for (c in 1..C)
+                    for (k in 1..K)
+                        for (x in 1..X)
+                            yield(inputVariableUsed[x])
+            }
+        }
     }
 }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
index 36a4f28b..2a10a27c 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
@@ -33,6 +33,7 @@ object Globals {
     var IS_ENCODE_TRANSITION_FUNCTION: Boolean = false
     var IS_ENCODE_EPSILON_PASSIVE: Boolean = false
     var IS_ENCODE_NOT_EPSILON_ACTIVE: Boolean = false
+    var IS_ENCODE_CONJUNCTIVE_GUARDS: Boolean = false
     var IS_FIX_ACTIVE: Boolean = false
     var IS_DEBUG: Boolean = false
     var IS_REUSE_K: Boolean = true

From 872708dbd9d6a5ce821b970b13e0005df05eb5be Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Sun, 17 Oct 2021 23:17:51 +0300
Subject: [PATCH 02/32] Add ConjunctiveGuard to SerializersModule

---
 .../ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt    | 4 ++++
 .../main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt   | 1 +
 2 files changed, 5 insertions(+)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt
index 3dbc67f9..c9062be4 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt
@@ -1,11 +1,15 @@
 package ru.ifmo.fbsat.core.automaton.guard
 
+import kotlinx.serialization.SerialName
+import kotlinx.serialization.Serializable
 import ru.ifmo.fbsat.core.scenario.InputValues
 import ru.ifmo.fbsat.core.utils.pow
 import ru.ifmo.fbsat.core.utils.toBinaryString
 import ru.ifmo.fbsat.core.utils.toBooleanList
 import kotlin.math.absoluteValue
 
+@Serializable
+@SerialName("ConjunctiveGuard")
 class ConjunctiveGuard(
     val literals: List<Int>, // signed 1-based
     val inputNames: List<String>,
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt
index 4c2309ec..e568d44d 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt
@@ -12,6 +12,7 @@ val guardModule = SerializersModule {
         subclass(TruthTableGuard::class)
         subclass(ParseTreeGuard::class)
         subclass(BooleanExpressionGuard::class)
+        subclass(ConjunctiveGuard::class)
     }
 }
 

From b5336f8ffa2065fe733759ef3410afcf63eb858d Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 18 Oct 2021 15:41:25 +0300
Subject: [PATCH 03/32] Add dumping of sliced scenarios after
 modular-parallel-basic inference with --encode-conjunctive-guards

---
 .../basic/parallel/ParallelModularBasic.kt    | 98 +++++++++++++++++++
 1 file changed, 98 insertions(+)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
index 9e410cd8..cb6de6f6 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
@@ -1,14 +1,31 @@
 package ru.ifmo.fbsat.core.task.modular.basic.parallel
 
+import com.github.lipen.multiarray.forEachIndexed
 import com.soywiz.klock.measureTimeWithResult
+import okio.buffer
+import okio.sink
 import ru.ifmo.fbsat.core.automaton.ParallelModularAutomaton
 import ru.ifmo.fbsat.core.automaton.buildBasicParallelModularAutomaton
+import ru.ifmo.fbsat.core.scenario.InputAction
+import ru.ifmo.fbsat.core.scenario.InputValues
+import ru.ifmo.fbsat.core.scenario.OutputAction
+import ru.ifmo.fbsat.core.scenario.OutputValues
+import ru.ifmo.fbsat.core.scenario.ScenarioElement
+import ru.ifmo.fbsat.core.scenario.positive.PositiveScenario
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
+import ru.ifmo.fbsat.core.solver.convertBoolVarArray
+import ru.ifmo.fbsat.core.solver.convertIntVarArray
 import ru.ifmo.fbsat.core.task.Inferrer
 import ru.ifmo.fbsat.core.task.optimizeParallelModularA
 import ru.ifmo.fbsat.core.task.optimizeParallelModularT
 import ru.ifmo.fbsat.core.utils.Globals
+import ru.ifmo.fbsat.core.utils.ModularContext
 import ru.ifmo.fbsat.core.utils.MyLogger
+import ru.ifmo.fbsat.core.utils.ensureParentExists
+import ru.ifmo.fbsat.core.utils.toBinaryString
+import ru.ifmo.fbsat.core.utils.useWith
+import ru.ifmo.fbsat.core.utils.write
+import ru.ifmo.fbsat.core.utils.writeln
 
 private val logger = MyLogger {}
 
@@ -74,10 +91,91 @@ fun Inferrer.parallelModularBasicMin(
     }
 }
 
+private fun PositiveScenario.slice(sliceInput: List<Int>, sliceOutput: List<Int>): PositiveScenario {
+    return PositiveScenario(elements = elements.map { it.slice(sliceInput, sliceOutput) })
+}
+
+private fun ScenarioElement.slice(sliceInput: List<Int>, sliceOutput: List<Int>): ScenarioElement {
+    return ScenarioElement(
+        inputAction = InputAction(
+            event = inputEvent,
+            values = inputValues.slice(sliceInput)
+        ),
+        outputAction = OutputAction(
+            event = outputEvent,
+            values = outputValues.slice(sliceOutput)
+        )
+    )
+}
+
+private fun InputValues.slice(sliceInput: List<Int>): InputValues {
+    return InputValues(values.slice(sliceInput.indices))
+}
+
+private fun OutputValues.slice(sliceInput: List<Int>): OutputValues {
+    return OutputValues(values.slice(sliceInput.indices))
+}
+
 fun Inferrer.inferParallelModularBasic(): ParallelModularAutomaton? {
     val model = solveAndGetModel() ?: return null
     val automaton = buildBasicParallelModularAutomaton(solver.context, model)
 
+    if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
+        val modularContext: ModularContext = solver.context["modularContext"]
+        val moduleControllingOutputVariable =
+            solver.context.convertIntVarArray("moduleControllingOutputVariable", model)
+        modularContext.forEachIndexed { (m), ctx ->
+            val scenarioTree: PositiveScenarioTree = ctx["scenarioTree"]
+            val X: Int = ctx["X"]
+            val Z: Int = ctx["Z"]
+            val inputVariableUsed = ctx.convertBoolVarArray("inputVariableUsed", model)
+
+            val sliceInput = (1..X).filter { x ->
+                inputVariableUsed[x]
+            }.map { it - 1 }
+            val sliceOutput = (1..Z).filter { z ->
+                moduleControllingOutputVariable[z] == m
+            }.map { it - 1 }
+            logger.debug("Slice input indices for m = $m: $sliceInput")
+            logger.debug("Slice output indices for m = $m: $sliceOutput")
+
+            val slicedScenarios = scenarioTree.scenarios.map {
+                it.slice(sliceInput, sliceOutput)
+            }
+            val outFile = outDir.resolve("sliced-scenarios-m$m")
+            logger.debug("Writing ${slicedScenarios.size} sliced scenario(s) for m = $m to '$outFile'")
+            outFile.ensureParentExists().sink().buffer().useWith {
+                writeln("${slicedScenarios.size}")
+                for (scenario in slicedScenarios) {
+                    for (element in scenario.elements) {
+                        if (element.inputEvent != null) {
+                            write("in=${element.inputEvent}[${element.inputValues.values.toBinaryString()}]; ")
+                        }
+                        if (element.outputEvent != null) {
+                            write("out=${element.outputEvent}[${element.outputValues.values.toBinaryString()}]; ")
+                        }
+                    }
+                    writeln()
+                }
+            }
+
+            outDir.resolve("input-names-m$m").ensureParentExists().sink().buffer().useWith {
+                for (x in 1..X) {
+                    if (inputVariableUsed[x]) {
+                        writeln(scenarioTree.inputNames[x - 1])
+                    }
+                }
+            }
+            outDir.resolve("output-names-m$m").ensureParentExists().sink().buffer().useWith {
+                for (z in 1..Z) {
+                    if (moduleControllingOutputVariable[z] == m) {
+                        writeln(scenarioTree.outputNames[z - 1])
+                    }
+                }
+            }
+        }
+    }
+
     // TODO: check automaton
     // log.warn("Mapping check is not implemented yet")
 

From 5681c21c3e255e5ba90a688a43bcaa61b8c282d9 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 19 Oct 2021 13:26:48 +0300
Subject: [PATCH 04/32] Fix(adhoc) Guard::truthTableString calculation for
 TruthTableGuard

---
 .../main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt | 5 ++++-
 .../kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt    | 8 ++++++--
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
index f7e7c73d..1366a77b 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
@@ -497,7 +497,10 @@ class Automaton(
             }
         val codeTransitionGuards =
             transitions.flatMap {
-                it.guard.truthTableString(inputNames)
+                val tt = it.guard.truthTableString(inputNames)
+                // FIXME: had to replace 'x' with '1' just to be able to compute hash of such guards,
+                //  but this should be fixed (rewritten) some time later...
+                tt.replace("x", "1")
                     .windowed(8, step = 8, partialWindows = true)
                     .map { s -> s.toInt(2) }
             }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt
index 5a6267ab..bd047fa9 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt
@@ -6,7 +6,6 @@ import kotlinx.serialization.modules.subclass
 import ru.ifmo.fbsat.core.scenario.InputValues
 import ru.ifmo.fbsat.core.utils.pow
 import ru.ifmo.fbsat.core.utils.toBinaryString
-import ru.ifmo.fbsat.core.utils.toBooleanList
 
 @Suppress("PublicApiImplicitType")
 val guardModule = SerializersModule {
@@ -29,5 +28,10 @@ interface Guard {
 
 fun Guard.truthTableString(inputNames: List<String>): String =
     (0 until 2.pow(inputNames.size)).map { i ->
-        eval(InputValues(i.toString(2).padStart(inputNames.size, '0').toBooleanList()))
+        val input = InputValues(i.toString(2).padStart(inputNames.size, '0'))
+        if (this is TruthTableGuard) {
+            this.truthTable[input]
+        } else {
+            eval(input)
+        }
     }.toBinaryString()

From 9d4ba76142bad4724c63199f1c5cd08785b7ae7a Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 19 Oct 2021 16:12:57 +0300
Subject: [PATCH 05/32] Add missing imports of extension props

---
 .../core/task/modular/basic/parallel/ParallelModularBasic.kt  | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
index cb6de6f6..4d2a7b55 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
@@ -11,6 +11,10 @@ import ru.ifmo.fbsat.core.scenario.InputValues
 import ru.ifmo.fbsat.core.scenario.OutputAction
 import ru.ifmo.fbsat.core.scenario.OutputValues
 import ru.ifmo.fbsat.core.scenario.ScenarioElement
+import ru.ifmo.fbsat.core.scenario.inputEvent
+import ru.ifmo.fbsat.core.scenario.inputValues
+import ru.ifmo.fbsat.core.scenario.outputEvent
+import ru.ifmo.fbsat.core.scenario.outputValues
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenario
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
 import ru.ifmo.fbsat.core.solver.convertBoolVarArray

From 1ec38bf77f0ac5f4c65dfeffbf1ea8ce8ffb28d3 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 19 Oct 2021 16:15:49 +0300
Subject: [PATCH 06/32] Fix cardinality and optimization

---
 .../cli/command/infer/AbstractInferCommand.kt |  1 +
 .../cli/command/infer/options/ExtraOptions.kt | 10 ++++
 .../ru/ifmo/fbsat/core/automaton/Automaton.kt | 16 +++++-
 .../automaton/ParallelModularAutomaton.kt     | 21 ++++----
 .../ru/ifmo/fbsat/core/task/Optimization.kt   | 35 ++++++++-----
 .../parallel/ParallelModularBasicVariables.kt | 50 ++++++++++++++++---
 .../fbsat/core/task/single/basic/Basic.kt     |  4 +-
 .../core/task/single/basic/BasicVariables.kt  | 16 ++++--
 .../ru/ifmo/fbsat/core/utils/Globals.kt       |  1 +
 9 files changed, 119 insertions(+), 35 deletions(-)

diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
index 6bea7866..b99b44a1 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
@@ -43,6 +43,7 @@ abstract class AbstractInferCommand<AutomatonType : Any>(name: String) : CliktCo
             Globals.IS_ENCODE_EPSILON_PASSIVE = isEncodeEpsilonPassive
             Globals.IS_ENCODE_NOT_EPSILON_ACTIVE = isEncodeNotEpsilonActive
             Globals.IS_ENCODE_CONJUNCTIVE_GUARDS = isEncodeConjunctiveGuards
+            Globals.IS_ENCODE_CARDINALITY_CKA = isEncodeCardinalityCKA
             Globals.IS_FIX_ACTIVE = isFixActive
             Globals.IS_REUSE_K = isReuseK
             Globals.IS_USE_ASSUMPTIONS = isUseAssumptions
diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
index 6b903240..5d9589ab 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
@@ -39,6 +39,7 @@ class ExtraOptions : OptionGroup(EXTRA_OPTIONS) {
     val isEncodeEpsilonPassive: Boolean by isEncodeEpsilonPassiveOption()
     val isEncodeNotEpsilonActive: Boolean by isEncodeNotEpsilonActiveOption()
     val isEncodeConjunctiveGuards: Boolean by isEncodeConjunctiveGuardsOption()
+    val isEncodeCardinalityCKA: Boolean by isEncodeCardinalityCKAOption()
     val isFixActive: Boolean by isFixActiveOption()
     val isReuseK: Boolean by isReuseKOption()
     val isUseAssumptions: Boolean by isUseAssumptionsOption()
@@ -254,6 +255,15 @@ fun ParameterHolder.isEncodeConjunctiveGuardsOption() =
         default = Globals.IS_ENCODE_CONJUNCTIVE_GUARDS
     )
 
+fun ParameterHolder.isEncodeCardinalityCKAOption() =
+    option(
+        "--encode-cardinality-CKA",
+        help = "Encode cardinalityCKA (just declare, but not use)"
+    ).flag(
+        "--no-encode-cardinality-CKA",
+        default = Globals.IS_ENCODE_CARDINALITY_CKA
+    )
+
 fun ParameterHolder.isFixActiveOption() =
     option(
         "--fix-active",
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
index 1366a77b..336ab790 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
@@ -536,7 +536,7 @@ class Automaton(
             ", P = $maxGuardSize" +
             ", T = $numberOfTransitions" +
             ", N = $totalGuardsSize" +
-            ", A = ${transitions.sumOf { (it.guard as? ConjunctiveGuard)?.literals?.size ?: 0 }}"
+            ", A = ${getA()}}"
     }
 
     fun printStats() {
@@ -984,3 +984,17 @@ fun buildExtendedAutomaton(
         }
     )
 }
+
+fun Automaton.getA(): Int? {
+    return (transitions.first().guard as? ConjunctiveGuard)?.literals?.size
+}
+
+fun Automaton.getTA(): Int? {
+    var sum = 0
+    for (t in transitions) {
+        val g = t.guard as? ConjunctiveGuard ?: return null
+        val a = g.literals.size
+        sum += a
+    }
+    return sum
+}
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
index 2eaed759..50c67867 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
@@ -177,17 +177,9 @@ class ParallelModularAutomaton(
             } = $totalGuardsSize" +
             ", A = ${
                 modules.values.joinToString("+") {
-                    it.transitions.sumOf {
-                        (it.guard as? ConjunctiveGuard)?.literals?.size ?: 0
-                    }.toString()
+                    it.getA()?.toString() ?: "?"
                 }
-            } = ${
-                modules.values.sumOf {
-                    it.transitions.sumOf {
-                        (it.guard as? ConjunctiveGuard)?.literals?.size ?: 0
-                    }
-                }
-            }"
+            } = ${getA() ?: "?"}"
     }
 
     fun printStats() {
@@ -486,3 +478,12 @@ fun buildExtendedParallelModularAutomaton(
 
     return ParallelModularAutomaton(modules, moduleControllingOutputVariable)
 }
+
+fun ParallelModularAutomaton.getA(): Int? {
+    var sum = 0
+    for (module in modules.values) {
+        val a = module.getA() ?: return null
+        sum += a
+    }
+    return sum
+}
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt
index 2e37253b..13317b4c 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt
@@ -7,7 +7,8 @@ import ru.ifmo.fbsat.core.automaton.Automaton
 import ru.ifmo.fbsat.core.automaton.ConsecutiveModularAutomaton
 import ru.ifmo.fbsat.core.automaton.DistributedAutomaton
 import ru.ifmo.fbsat.core.automaton.ParallelModularAutomaton
-import ru.ifmo.fbsat.core.automaton.guard.ConjunctiveGuard
+import ru.ifmo.fbsat.core.automaton.getA
+import ru.ifmo.fbsat.core.automaton.getTA
 import ru.ifmo.fbsat.core.task.distributed.basic.inferDistributedBasic
 import ru.ifmo.fbsat.core.task.distributed.complete.inferDistributedComplete
 import ru.ifmo.fbsat.core.task.distributed.extended.inferDistributedExtended
@@ -116,23 +117,19 @@ fun Inferrer.optimizeN(
 }
 
 @Suppress("FunctionName")
-fun Inferrer.optimizeA(
+fun Inferrer.optimizeTA(
     start: Int? = null,
     end: Int = 0,
     useAssumptions: Boolean = Globals.IS_USE_ASSUMPTIONS,
 ): Automaton? {
-    logger.info("Optimizing A (${if (useAssumptions) "with" else "without"} assumptions) from $start to $end...")
-    val cardinality: Cardinality = solver.context["cardinalityA"]
+    logger.info("Optimizing T*A (${if (useAssumptions) "with" else "without"} assumptions) from $start to $end...")
+    val cardinality: Cardinality = solver.context["cardinalityTA"]
     return cardinality.optimizeTopDown(
         start = start,
         end = end,
         useAssumptions = useAssumptions,
         infer = { inferBasic() },
-        query = {
-            it.transitions.sumOf { t ->
-                (t.guard as ConjunctiveGuard).literals.size
-            }
-        }
+        query = { it.getTA()!! }
     )
 }
 
@@ -273,6 +270,22 @@ fun Inferrer.optimizeParallelModularA(
 ): ParallelModularAutomaton? {
     logger.info("Optimizing A (${if (useAssumptions) "with" else "without"} assumptions) from $start to $end...")
     val cardinality: Cardinality = solver.context["cardinalityA"]
+    return cardinality.optimizeTopDown(
+        start = start,
+        end = end,
+        useAssumptions = useAssumptions,
+        infer = { inferParallelModularBasic() },
+        query = { it.getA()!! }
+    )
+}
+
+fun Inferrer.optimizeParallelModularCKA(
+    start: Int? = null,
+    end: Int = 0,
+    useAssumptions: Boolean = Globals.IS_USE_ASSUMPTIONS,
+): ParallelModularAutomaton? {
+    logger.info("Optimizing C*K*A (${if (useAssumptions) "with" else "without"} assumptions) from $start to $end...")
+    val cardinality: Cardinality = solver.context["cardinalityCKA"]
     return cardinality.optimizeTopDown(
         start = start,
         end = end,
@@ -280,9 +293,7 @@ fun Inferrer.optimizeParallelModularA(
         infer = { inferParallelModularBasic() },
         query = {
             it.modules.values.sumOf { module ->
-                module.transitions.sumOf { t ->
-                    (t.guard as ConjunctiveGuard).literals.size
-                }
+                module.numberOfTransitions * module.maxOutgoingTransitions * module.getA()!!
             }
         }
     )
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
index 4e794b3d..8d1ecdbb 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
@@ -74,16 +74,54 @@ fun Solver.declareParallelModularBasicVariables(
             declareCardinality {
                 @Suppress("NAME_SHADOWING")
                 forEachModularContext {
-                    val C: Int = context["C"]
-                    val K: Int = context["K"]
                     val X: Int = context["X"]
                     val inputVariableUsed: BoolVarArray = context["inputVariableUsed"]
-                    for (c in 1..C)
-                        for (k in 1..K)
-                            for (x in 1..X)
-                                yield(inputVariableUsed[x])
+                    for (x in 1..X)
+                        yield(inputVariableUsed[x])
                 }
             }
         }
+        if (Globals.IS_ENCODE_CARDINALITY_CKA) {
+            comment("Cardinality (C*K*A)")
+            val cardinalityCKA = context("cardinalityCKA") {
+                declareCardinality {
+                    @Suppress("NAME_SHADOWING")
+                    forEachModularContext {
+                        val C: Int = context["C"]
+                        val K: Int = context["K"]
+                        val X: Int = context["X"]
+                        val inputVariableUsed: BoolVarArray = context["inputVariableUsed"]
+                        for (c in 1..C)
+                            for (k in 1..K)
+                                for (x in 1..X)
+                                    yield(inputVariableUsed[x])
+                    }
+                }
+            }
+        }
+        // comment("Cardinality (T*A)")
+        // val cardinalityTA = context("cardinalityTA") {
+        //     declareCardinality {
+        //         @Suppress("NAME_SHADOWING")
+        //         forEachModularContext {
+        //             val C: Int = context["C"]
+        //             val K: Int = context["K"]
+        //             val X: Int = context["X"]
+        //             val transitionDestination: IntVarArray = context["transitionDestination"]
+        //             val inputVariableUsed: BoolVarArray = context["inputVariableUsed"]
+        //             for (c in 1..C)
+        //                 for (k in 1..K)
+        //                     for (x in 1..X) {
+        //                         val aux = newLiteral()
+        //                         iffAnd(
+        //                             aux,
+        //                             transitionDestination[c, k] neq 0,
+        //                             inputVariableUsed[x]
+        //                         )
+        //                         yield(aux)
+        //                     }
+        //         }
+        //     }
+        // }
     }
 }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt
index db485342..e023266c 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt
@@ -10,7 +10,7 @@ import ru.ifmo.fbsat.core.solver.numberOfConflicts
 import ru.ifmo.fbsat.core.solver.numberOfDecisions
 import ru.ifmo.fbsat.core.solver.numberOfPropagations
 import ru.ifmo.fbsat.core.task.Inferrer
-import ru.ifmo.fbsat.core.task.optimizeA
+import ru.ifmo.fbsat.core.task.optimizeTA
 import ru.ifmo.fbsat.core.task.optimizeT
 import ru.ifmo.fbsat.core.utils.Globals
 import ru.ifmo.fbsat.core.utils.MyLogger
@@ -103,7 +103,7 @@ fun Inferrer.basicMin(
             isEncodeReverseImplication = isEncodeReverseImplication
         ) ?: return@run null
         if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
-            optimizeA()
+            optimizeTA()
         } else {
             optimizeT()
         }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
index f8e36616..84f27fc2 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
@@ -8,6 +8,7 @@ import com.github.lipen.satlib.core.neq
 import com.github.lipen.satlib.core.newBoolVarArray
 import com.github.lipen.satlib.core.newIntVar
 import com.github.lipen.satlib.core.newIntVarArray
+import com.github.lipen.satlib.op.iffAnd
 import com.github.lipen.satlib.solver.Solver
 import ru.ifmo.fbsat.core.scenario.initialOutputValues
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
@@ -128,14 +129,21 @@ fun Solver.declareBasicVariables(
         }
     }
     if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
-        comment("Cardinality (A)")
+        comment("Cardinality (T*A)")
         val inputVariableUsed: BoolVarArray = context["inputVariableUsed"]
-        val cardinalityA = context("cardinalityA") {
+        val cardinalityTA = context("cardinalityTA") {
             declareCardinality {
                 for (c in 1..C)
                     for (k in 1..K)
-                        for (x in 1..X)
-                            yield(inputVariableUsed[x])
+                        for (x in 1..X) {
+                            val aux = newLiteral()
+                            iffAnd(
+                                aux,
+                                transitionDestination[c, k] neq 0,
+                                inputVariableUsed[x]
+                            )
+                            yield(aux)
+                        }
             }
         }
     }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
index 2a10a27c..10ecef8e 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
@@ -34,6 +34,7 @@ object Globals {
     var IS_ENCODE_EPSILON_PASSIVE: Boolean = false
     var IS_ENCODE_NOT_EPSILON_ACTIVE: Boolean = false
     var IS_ENCODE_CONJUNCTIVE_GUARDS: Boolean = false
+    var IS_ENCODE_CARDINALITY_CKA: Boolean = false
     var IS_FIX_ACTIVE: Boolean = false
     var IS_DEBUG: Boolean = false
     var IS_REUSE_K: Boolean = true

From 1a7a5a80faaa34eb6089d53a5f5510588f4c61ae Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 19 Oct 2021 17:40:05 +0300
Subject: [PATCH 07/32] Remove unnecessary comma

---
 .../ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt    | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
index 50c67867..b87c92be 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
@@ -153,7 +153,7 @@ class ParallelModularAutomaton(
     }
 
     fun getStats(): String {
-        return "M = $numberOfModules, " +
+        return "M = $numberOfModules" +
             ", C = ${
                 modules.values.joinToString("+") {
                     it.numberOfStates.toString()

From bfaa96ceb1926e7818937bc43fa50888ea9a32c0 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 20 Oct 2021 11:28:05 +0300
Subject: [PATCH 08/32] Add --fixed-output-decomposition option

---
 .../fbsat/cli/command/infer/AbstractInferCommand.kt  |  1 +
 .../fbsat/cli/command/infer/options/ExtraOptions.kt  | 12 ++++++++++++
 .../constraints/AutomatonStructureConstraints.kt     | 10 ++++++++++
 .../main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt  |  1 +
 4 files changed, 24 insertions(+)

diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
index b99b44a1..2392e7e1 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
@@ -24,6 +24,7 @@ abstract class AbstractInferCommand<AutomatonType : Any>(name: String) : CliktCo
         with(extraOptions) {
             Globals.EPSILON_OUTPUT_EVENTS = epsilonOutputEvents
             Globals.START_STATE_ALGORITHMS = startStateAlgorithms
+            Globals.FIXED_OUTPUT_DECOMPOSITION = fixedOutputDecomposition
             Globals.IS_FORBID_OR = isForbidOr
             Globals.IS_FORBID_TRANSITIONS_TO_FIRST_STATE = isForbidTransitionsToFirstState
             Globals.IS_BFS_AUTOMATON = isBfsAutomaton
diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
index 5d9589ab..34fac4e3 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
@@ -24,6 +24,7 @@ class ExtraOptions : OptionGroup(EXTRA_OPTIONS) {
     val isBfsGuard: Boolean by isBfsGuardOption()
     val epsilonOutputEvents: EpsilonOutputEvents by getEpsilonOutputEventsOption()
     val startStateAlgorithms: StartStateAlgorithms by getStartStateAlgorithmsOption()
+    val fixedOutputDecomposition: List<Int?>? by getFixedOutputDecompositionOption()
     val isEncodeReverseImplication: Boolean by isEncodeReverseImplicationOption()
     val isEncodeTransitionsOrder: Boolean by isEncodeTransitionsOrderOption()
     val isEncodeTerminalsOrder: Boolean by isEncodeTerminalsOrderOption()
@@ -120,6 +121,17 @@ fun ParameterHolder.getStartStateAlgorithmsOption() =
         Globals.START_STATE_ALGORITHMS
     )
 
+fun ParameterHolder.getFixedOutputDecompositionOption() =
+    option(
+        "--fixed-output-decomposition",
+        help = "[modular-parallel] Comma-separated modules (1-based), controlling output variables"
+    ).convert {
+        require(it.isNotBlank()) { "string should not be blank" }
+        it.split(",").map { s ->
+            s.trim().toIntOrNull()
+        }
+    }
+
 fun ParameterHolder.isEncodeReverseImplicationOption() =
     option(
         "--encode-reverse-implication",
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index 265e0cc8..27349568 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -90,6 +90,16 @@ fun Solver.declareParallelModularAutomatonStructureConstraints() {
                 imply(moduleControllingOutputVariable[z] neq m, -stateAlgorithmBot[c, z])
             }
     }
+
+    if (Globals.FIXED_OUTPUT_DECOMPOSITION != null) {
+        comment("(adhoc) Fixing output decomposition")
+        for (z in 1..Z) {
+            val m = Globals.FIXED_OUTPUT_DECOMPOSITION!![z - 1]
+            if (m != null) {
+                clause(moduleControllingOutputVariable[z] eq m)
+            }
+        }
+    }
 }
 
 fun Solver.declareConsecutiveModularAutomatonStructureConstraints() {
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
index 10ecef8e..70d4c081 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
@@ -15,6 +15,7 @@ enum class StartStateAlgorithms {
 object Globals {
     var EPSILON_OUTPUT_EVENTS: EpsilonOutputEvents = EpsilonOutputEvents.ONLYSTART
     var START_STATE_ALGORITHMS: StartStateAlgorithms = StartStateAlgorithms.ZERO
+    var FIXED_OUTPUT_DECOMPOSITION: List<Int?>? = null
     var IS_FORBID_OR: Boolean = false
     var IS_FORBID_TRANSITIONS_TO_FIRST_STATE: Boolean = true
     var IS_BFS_AUTOMATON: Boolean = true

From 5d2752adeeb75c358b652dfc837e5c07e5e43491 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 20 Oct 2021 11:30:16 +0300
Subject: [PATCH 09/32] Remove unnecessary extension methods

---
 .../basic/parallel/ParallelModularBasic.kt    | 31 -------------------
 1 file changed, 31 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
index 4d2a7b55..aa3024f1 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
@@ -6,16 +6,10 @@ import okio.buffer
 import okio.sink
 import ru.ifmo.fbsat.core.automaton.ParallelModularAutomaton
 import ru.ifmo.fbsat.core.automaton.buildBasicParallelModularAutomaton
-import ru.ifmo.fbsat.core.scenario.InputAction
-import ru.ifmo.fbsat.core.scenario.InputValues
-import ru.ifmo.fbsat.core.scenario.OutputAction
-import ru.ifmo.fbsat.core.scenario.OutputValues
-import ru.ifmo.fbsat.core.scenario.ScenarioElement
 import ru.ifmo.fbsat.core.scenario.inputEvent
 import ru.ifmo.fbsat.core.scenario.inputValues
 import ru.ifmo.fbsat.core.scenario.outputEvent
 import ru.ifmo.fbsat.core.scenario.outputValues
-import ru.ifmo.fbsat.core.scenario.positive.PositiveScenario
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
 import ru.ifmo.fbsat.core.solver.convertBoolVarArray
 import ru.ifmo.fbsat.core.solver.convertIntVarArray
@@ -95,31 +89,6 @@ fun Inferrer.parallelModularBasicMin(
     }
 }
 
-private fun PositiveScenario.slice(sliceInput: List<Int>, sliceOutput: List<Int>): PositiveScenario {
-    return PositiveScenario(elements = elements.map { it.slice(sliceInput, sliceOutput) })
-}
-
-private fun ScenarioElement.slice(sliceInput: List<Int>, sliceOutput: List<Int>): ScenarioElement {
-    return ScenarioElement(
-        inputAction = InputAction(
-            event = inputEvent,
-            values = inputValues.slice(sliceInput)
-        ),
-        outputAction = OutputAction(
-            event = outputEvent,
-            values = outputValues.slice(sliceOutput)
-        )
-    )
-}
-
-private fun InputValues.slice(sliceInput: List<Int>): InputValues {
-    return InputValues(values.slice(sliceInput.indices))
-}
-
-private fun OutputValues.slice(sliceInput: List<Int>): OutputValues {
-    return OutputValues(values.slice(sliceInput.indices))
-}
-
 fun Inferrer.inferParallelModularBasic(): ParallelModularAutomaton? {
     val model = solveAndGetModel() ?: return null
     val automaton = buildBasicParallelModularAutomaton(solver.context, model)

From f13f26d85b49ce5b19caa7f9e23b442d3fdd33b2 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 20 Oct 2021 11:45:30 +0300
Subject: [PATCH 10/32] Fix typo

---
 .../fbsat/core/constraints/AutomatonStructureConstraints.kt     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index 27349568..31c6db5e 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -462,7 +462,7 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs(
         val inputVariableLiteral: BoolVarArray = context["inputVariableLiteral"]
 
         comment("Conjunctive guards")
-        // tt[c,k,u] <=> AND_{x}(used[x] => (lit[c,k,x] <=> u[x])
+        // tt[c,k,u] <=> AND_{x}(used[x] => (lit[c,k,x] <=> u[x]))
         for (c in 1..C)
             for (k in 1..K)
                 for (u in Us)

From 6cf3ba50b052f25d4cac46ad951358921bcadca5 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 20 Oct 2021 12:00:08 +0300
Subject: [PATCH 11/32] Fix free variables

---
 .../core/constraints/AutomatonStructureConstraints.kt  | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index 31c6db5e..03f40ea8 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -486,5 +486,15 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs(
                         -inputVariableUsed[x],
                         -inputVariableLiteral[c, k, x]
                     )
+
+        // fix free variables
+        // (transitionDestination[c,k] = 0) => lit[c,k,x]
+        for (c in 1..C)
+            for (k in 1..K)
+                for (x in 1..X)
+                    imply(
+                        transitionDestination[c, k] eq 0,
+                        inputVariableLiteral[c, k, x]
+                    )
     }
 }

From b7f6904fecc1cd7ca8d8899fd6de8227900e5f5a Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 20 Oct 2021 14:07:12 +0300
Subject: [PATCH 12/32] Remove UNNECESSARY constraint. Add ALO(used)

---
 .../AutomatonStructureConstraints.kt          | 26 ++++++++++++-------
 1 file changed, 16 insertions(+), 10 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index 03f40ea8..fdd273c0 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -461,7 +461,7 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs(
         val inputVariableUsed: BoolVarArray = context["inputVariableUsed"]
         val inputVariableLiteral: BoolVarArray = context["inputVariableLiteral"]
 
-        comment("Conjunctive guards")
+        comment("Conjunctive guard definition")
         // tt[c,k,u] <=> AND_{x}(used[x] => (lit[c,k,x] <=> u[x]))
         for (c in 1..C)
             for (k in 1..K)
@@ -477,17 +477,23 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs(
                             yield(aux)
                         }
                     }
-
         // ~used[x] => ~lit[c,k,x]
-        for (c in 1..C)
-            for (k in 1..K)
-                for (x in 1..X)
-                    imply(
-                        -inputVariableUsed[x],
-                        -inputVariableLiteral[c, k, x]
-                    )
+        // for (c in 1..C)
+        //     for (k in 1..K)
+        //         for (x in 1..X)
+        //             imply(
+        //                 -inputVariableUsed[x],
+        //                 -inputVariableLiteral[c, k, x]
+        //             )
+
+        comment("ALO inputVariableUsed")
+        // ALO_{x}(used[x])
+        atLeastOne {
+            for (x in 1..X)
+                yield(inputVariableUsed[x])
+        }
 
-        // fix free variables
+        comment("Fix free variables")
         // (transitionDestination[c,k] = 0) => lit[c,k,x]
         for (c in 1..C)
             for (k in 1..K)

From da0ab0dbe627fc921ccaebbfa2bcca9a4874daaa Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 20 Oct 2021 17:29:06 +0300
Subject: [PATCH 13/32] Add logging of output decomposition

---
 .../parallel/AbstractInferParallelModularCommand.kt       | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/AbstractInferParallelModularCommand.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/AbstractInferParallelModularCommand.kt
index 7ba04292..763f0bfd 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/AbstractInferParallelModularCommand.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/AbstractInferParallelModularCommand.kt
@@ -16,14 +16,16 @@ abstract class AbstractInferParallelModularCommand(name: String) :
         } else {
             logger.info("Inferred parallel modular automaton consists of ${automaton.modules.shape.single()} modules:")
             for ((m, module) in automaton.modules.values.withIndex(start = 1)) {
-                logger.info("Module #$m (${module.getStats()}):")
+                logger.info("Module #$m (${module.getStats()}, vars = ${automaton.moduleOutputVariables[m]}):")
                 module.pprint()
             }
+            logger.info("Output decomposition: ${automaton.outputVariableModule.values}")
+            for (m in 1..automaton.M) {
+                logger.info("    m = $m: ${automaton.moduleOutputVariables[m]}")
+            }
             logger.info("Inferred parallel modular automaton has:")
             automaton.printStats()
 
-            // TODO: print controlled variables of each module
-
             // TODO: automaton.dump(outDir)
 
             if (automaton.verify(scenarioTree.toOld()))

From f4f1b6148a3068a385b3ccb9642433a0108e6144 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 20 Oct 2021 21:40:46 +0300
Subject: [PATCH 14/32] Fix typo

---
 .../fbsat/core/constraints/AutomatonStructureConstraints.kt     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index fdd273c0..90736159 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -79,7 +79,7 @@ fun Solver.declareParallelModularAutomatonStructureConstraints() {
                 yield(moduleControllingOutputVariable[z] eq m)
         }
 
-    comment("Constraint free variables")
+    comment("Constrain free variables")
     forEachModularContext { m ->
         val C: Int = context["C"]
         val stateAlgorithmBot: BoolVarArray = context["stateAlgorithmBot"]

From 843fd67b487ee08bcfd4421681e1560a59ab48b1 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 20 Oct 2021 21:41:33 +0300
Subject: [PATCH 15/32] Add constraint for 0-guards on null-transitions

---
 .../core/constraints/AutomatonStructureConstraints.kt    | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index 90736159..55ed252b 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -443,6 +443,15 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs(
         }
     }
 
+    comment("Null-transitions have False guards")
+    for (c in 1..C)
+        for (k in 1..K)
+            for (u in Us)
+                imply(
+                    transitionDestination[c,k] eq 0,
+                    -transitionTruthTable[c,k,u]
+                )
+
     if (Globals.IS_ENCODE_DISJUNCTIVE_TRANSITIONS) {
         comment("Transitions are disjunctive (without priority function)")
         for (c in 1..C)

From a50ecef0efd304fb95ed74d527841f9785dd8a00 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 21 Oct 2021 13:11:22 +0300
Subject: [PATCH 16/32] Add implication (tau!=0) to conjunctive guard
 definition

---
 .../core/constraints/AutomatonStructureConstraints.kt     | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index 55ed252b..73b0ca89 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -15,6 +15,7 @@ import com.github.lipen.satlib.op.iffAnd
 import com.github.lipen.satlib.op.iffImply
 import com.github.lipen.satlib.op.imply
 import com.github.lipen.satlib.op.implyAnd
+import com.github.lipen.satlib.op.implyIffAnd
 import com.github.lipen.satlib.op.implyOr
 import com.github.lipen.satlib.solver.Solver
 import ru.ifmo.fbsat.core.scenario.InputValues
@@ -471,11 +472,14 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs(
         val inputVariableLiteral: BoolVarArray = context["inputVariableLiteral"]
 
         comment("Conjunctive guard definition")
-        // tt[c,k,u] <=> AND_{x}(used[x] => (lit[c,k,x] <=> u[x]))
+        // (transitionDestination[c,k] != 0) => (tt[c,k,u] <=> AND_{x}(used[x] => (lit[c,k,x] <=> u[x])))
         for (c in 1..C)
             for (k in 1..K)
                 for (u in Us)
-                    iffAnd(transitionTruthTable[c, k, u]) {
+                    implyIffAnd(
+                        transitionDestination[c, k] neq 0,
+                        transitionTruthTable[c, k, u]
+                    ) {
                         for (x in 1..X) {
                             val aux = newLiteral()
                             iffImply(

From 179fa33aa2a70f8c8edd488ed2e0f89794d494da Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 21 Oct 2021 13:12:05 +0300
Subject: [PATCH 17/32] Fix automaton mapping in eventless case

---
 .../main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt  | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
index 336ab790..974fd348 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
@@ -25,6 +25,7 @@ import ru.ifmo.fbsat.core.scenario.Scenario
 import ru.ifmo.fbsat.core.scenario.inputActionsSeq
 import ru.ifmo.fbsat.core.scenario.negative.NegativeScenario
 import ru.ifmo.fbsat.core.scenario.negative.OldNegativeScenarioTree
+import ru.ifmo.fbsat.core.scenario.outputValues
 import ru.ifmo.fbsat.core.scenario.positive.OldPositiveScenarioTree
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenario
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
@@ -332,8 +333,10 @@ class Automaton(
         out@ for ((i, result) in eval(scenario).withIndex()) {
             val element = scenario.elements[i]
             if (result.outputAction != element.outputAction) {
-                logger.error("No mapping for ${i + 1}-th element = $element, result = $result")
-                break@out
+                if (!Globals.IS_ENCODE_EVENTLESS || result.outputAction.values != element.outputValues) {
+                    logger.error("No mapping for ${i + 1}-th element = $element, result = $result")
+                    break@out
+                }
             }
             mapping[i] = result
         }

From 5a7bf44d1448c164eb4b0c8f5e48562ece6c6f41 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 21 Oct 2021 13:13:00 +0300
Subject: [PATCH 18/32] Add some logging, cleanup

---
 .../kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt |  2 --
 .../fbsat/core/automaton/ParallelModularAutomaton.kt |  2 --
 .../constraints/AutomatonStructureConstraints.kt     | 12 ++----------
 .../modular/basic/parallel/ParallelModularBasic.kt   | 12 ++++--------
 .../basic/parallel/ParallelModularBasicVariables.kt  |  9 +++++++++
 .../fbsat/core/task/single/basic/BasicVariables.kt   |  9 +++++++++
 6 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
index 974fd348..762f2c84 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt
@@ -894,8 +894,6 @@ fun buildBasicAutomaton(
         },
         transitionGuard = { c, k ->
             if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
-                // inputVariableUsed!!
-                // inputVariableLiteral!!
                 ConjunctiveGuard(
                     literals = (1..X)
                         .filter { x -> inputVariableUsed[x] }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
index b87c92be..087a9e34 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
@@ -381,8 +381,6 @@ fun buildBasicParallelModularAutomaton(
             },
             transitionGuard = { c, k ->
                 if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
-                    // inputVariableUsed!!
-                    // inputVariableLiteral!!
                     ConjunctiveGuard(
                         literals = (1..X)
                             .filter { x -> inputVariableUsed[x] }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index 73b0ca89..000dc609 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -449,8 +449,8 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs(
         for (k in 1..K)
             for (u in Us)
                 imply(
-                    transitionDestination[c,k] eq 0,
-                    -transitionTruthTable[c,k,u]
+                    transitionDestination[c, k] eq 0,
+                    -transitionTruthTable[c, k, u]
                 )
 
     if (Globals.IS_ENCODE_DISJUNCTIVE_TRANSITIONS) {
@@ -490,14 +490,6 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs(
                             yield(aux)
                         }
                     }
-        // ~used[x] => ~lit[c,k,x]
-        // for (c in 1..C)
-        //     for (k in 1..K)
-        //         for (x in 1..X)
-        //             imply(
-        //                 -inputVariableUsed[x],
-        //                 -inputVariableLiteral[c, k, x]
-        //             )
 
         comment("ALO inputVariableUsed")
         // ALO_{x}(used[x])
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
index aa3024f1..b24cd9e0 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
@@ -133,17 +133,13 @@ fun Inferrer.inferParallelModularBasic(): ParallelModularAutomaton? {
             }
 
             outDir.resolve("input-names-m$m").ensureParentExists().sink().buffer().useWith {
-                for (x in 1..X) {
-                    if (inputVariableUsed[x]) {
-                        writeln(scenarioTree.inputNames[x - 1])
-                    }
+                for (name in scenarioTree.inputNames.slice(sliceInput)) {
+                    writeln(name)
                 }
             }
             outDir.resolve("output-names-m$m").ensureParentExists().sink().buffer().useWith {
-                for (z in 1..Z) {
-                    if (moduleControllingOutputVariable[z] == m) {
-                        writeln(scenarioTree.outputNames[z - 1])
-                    }
+                for (name in scenarioTree.outputNames.slice(sliceOutput)) {
+                    writeln(name)
                 }
             }
         }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
index 8d1ecdbb..5ce58b99 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
@@ -11,6 +11,9 @@ import ru.ifmo.fbsat.core.solver.declareModularContext
 import ru.ifmo.fbsat.core.solver.forEachModularContext
 import ru.ifmo.fbsat.core.task.single.basic.declareBasicVariables
 import ru.ifmo.fbsat.core.utils.Globals
+import ru.ifmo.fbsat.core.utils.MyLogger
+
+private val logger = MyLogger {}
 
 @Suppress("LocalVariableName")
 fun Solver.declareParallelModularBasicVariables(
@@ -71,6 +74,8 @@ fun Solver.declareParallelModularBasicVariables(
     if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
         comment("Cardinality (A)")
         val cardinalityA = context("cardinalityA") {
+            val nVars = numberOfVariables
+            val nCons = numberOfClauses
             declareCardinality {
                 @Suppress("NAME_SHADOWING")
                 forEachModularContext {
@@ -79,6 +84,10 @@ fun Solver.declareParallelModularBasicVariables(
                     for (x in 1..X)
                         yield(inputVariableUsed[x])
                 }
+            }.also {
+                val diffVars = numberOfVariables - nVars
+                val diffCons = numberOfClauses - nCons
+                logger.debug("Declared cardinalityA: $diffVars vars and $diffCons clauses")
             }
         }
         if (Globals.IS_ENCODE_CARDINALITY_CKA) {
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
index 84f27fc2..4568f2e3 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
@@ -13,6 +13,9 @@ import com.github.lipen.satlib.solver.Solver
 import ru.ifmo.fbsat.core.scenario.initialOutputValues
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
 import ru.ifmo.fbsat.core.utils.Globals
+import ru.ifmo.fbsat.core.utils.MyLogger
+
+private val logger = MyLogger {}
 
 @Suppress("LocalVariableName")
 fun Solver.declareBasicVariables(
@@ -132,6 +135,8 @@ fun Solver.declareBasicVariables(
         comment("Cardinality (T*A)")
         val inputVariableUsed: BoolVarArray = context["inputVariableUsed"]
         val cardinalityTA = context("cardinalityTA") {
+            val nVars = numberOfVariables
+            val nCons = numberOfClauses
             declareCardinality {
                 for (c in 1..C)
                     for (k in 1..K)
@@ -144,6 +149,10 @@ fun Solver.declareBasicVariables(
                             )
                             yield(aux)
                         }
+            }.also {
+                val diffVars = numberOfVariables - nVars
+                val diffCons = numberOfClauses - nCons
+                logger.debug("Declared cardinalityTA: $diffVars vars and $diffCons clauses")
             }
         }
     }

From 5e4ae84fc17725621a9839cdc68916597713d0df Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 21 Oct 2021 14:10:07 +0300
Subject: [PATCH 19/32] Add stub for --fix-output-decomposition flag

---
 .../fbsat/cli/command/infer/AbstractInferCommand.kt    |  1 +
 .../fbsat/cli/command/infer/options/ExtraOptions.kt    | 10 ++++++++++
 .../main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt    |  1 +
 3 files changed, 12 insertions(+)

diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
index 2392e7e1..2da3a237 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
@@ -46,6 +46,7 @@ abstract class AbstractInferCommand<AutomatonType : Any>(name: String) : CliktCo
             Globals.IS_ENCODE_CONJUNCTIVE_GUARDS = isEncodeConjunctiveGuards
             Globals.IS_ENCODE_CARDINALITY_CKA = isEncodeCardinalityCKA
             Globals.IS_FIX_ACTIVE = isFixActive
+            Globals.IS_FIX_OUTPUT_DECOMPOSITION = isFixOutputDecomposition
             Globals.IS_REUSE_K = isReuseK
             Globals.IS_USE_ASSUMPTIONS = isUseAssumptions
             Globals.IS_RENDER_WITH_DOT = isRenderWithDot
diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
index 34fac4e3..16c74545 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
@@ -42,6 +42,7 @@ class ExtraOptions : OptionGroup(EXTRA_OPTIONS) {
     val isEncodeConjunctiveGuards: Boolean by isEncodeConjunctiveGuardsOption()
     val isEncodeCardinalityCKA: Boolean by isEncodeCardinalityCKAOption()
     val isFixActive: Boolean by isFixActiveOption()
+    val isFixOutputDecomposition: Boolean by isFixOutputDecompositionOption()
     val isReuseK: Boolean by isReuseKOption()
     val isUseAssumptions: Boolean by isUseAssumptionsOption()
     val isRenderWithDot: Boolean by isRenderWithDotOption()
@@ -285,6 +286,15 @@ fun ParameterHolder.isFixActiveOption() =
         default = Globals.IS_FIX_ACTIVE
     )
 
+fun ParameterHolder.isFixOutputDecompositionOption() =
+    option(
+        "--fix-output-decomposition",
+        help = "Fix moduleControllingOutputVariable after modular-parallel-basic-minC"
+    ).flag(
+        "--no-fix-output-decomposition",
+        default = Globals.IS_FIX_OUTPUT_DECOMPOSITION
+    )
+
 fun ParameterHolder.isReuseKOption() =
     option(
         "--reuse-k",
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
index 70d4c081..eecef830 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
@@ -37,6 +37,7 @@ object Globals {
     var IS_ENCODE_CONJUNCTIVE_GUARDS: Boolean = false
     var IS_ENCODE_CARDINALITY_CKA: Boolean = false
     var IS_FIX_ACTIVE: Boolean = false
+    var IS_FIX_OUTPUT_DECOMPOSITION: Boolean = false
     var IS_DEBUG: Boolean = false
     var IS_REUSE_K: Boolean = true
     var IS_DUMP_CNF: Boolean = false

From c65640854f23b4f46cb17aad3c7bf6cbd27cff2f Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 21 Oct 2021 17:00:50 +0300
Subject: [PATCH 20/32] Add maxOutgoingTransitions option for
 parallel-modular-basic tasks

---
 .../modular/parallel/InferParallelModularBasicMin.kt |  5 ++++-
 .../parallel/InferParallelModularBasicMinC.kt        |  5 ++++-
 .../modular/basic/parallel/ParallelModularBasic.kt   | 12 ++++++++++--
 3 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMin.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMin.kt
index dd2f5a8c..b784c67d 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMin.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMin.kt
@@ -11,6 +11,7 @@ import ru.ifmo.fbsat.cli.command.infer.options.INPUT_OUTPUT_OPTIONS
 import ru.ifmo.fbsat.cli.command.infer.options.SolverOptions
 import ru.ifmo.fbsat.cli.command.infer.options.getInitialOutputValuesOption
 import ru.ifmo.fbsat.cli.command.infer.options.inputNamesOption
+import ru.ifmo.fbsat.cli.command.infer.options.maxOutgoingTransitionsOption
 import ru.ifmo.fbsat.cli.command.infer.options.numberOfModulesOption
 import ru.ifmo.fbsat.cli.command.infer.options.numberOfStatesOption
 import ru.ifmo.fbsat.cli.command.infer.options.outDirOption
@@ -32,6 +33,7 @@ private class ParallelModularBasicMinInputOutputOptions : OptionGroup(INPUT_OUTP
 private class ParallelModularBasicMinAutomatonOptions : OptionGroup(AUTOMATON_OPTIONS) {
     val numberOfModules: Int by numberOfModulesOption().required()
     val numberOfStates: Int? by numberOfStatesOption()
+    val maxOutgoingTransitions: Int? by maxOutgoingTransitionsOption()
 }
 
 class InferParallelModularBasicMinCommand :
@@ -51,6 +53,7 @@ class InferParallelModularBasicMinCommand :
         inferrer.parallelModularBasicMin(
             scenarioTree = scenarioTree,
             numberOfModules = params.numberOfModules,
-            numberOfStates = params.numberOfStates
+            numberOfStates = params.numberOfStates,
+            maxOutgoingTransitionsForC = { params.maxOutgoingTransitions ?: it }
         )
 }
diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMinC.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMinC.kt
index 75deb7c6..3729d4c3 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMinC.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMinC.kt
@@ -13,6 +13,7 @@ import ru.ifmo.fbsat.cli.command.infer.options.SolverOptions
 import ru.ifmo.fbsat.cli.command.infer.options.endNumberOfStatesOption
 import ru.ifmo.fbsat.cli.command.infer.options.getInitialOutputValuesOption
 import ru.ifmo.fbsat.cli.command.infer.options.inputNamesOption
+import ru.ifmo.fbsat.cli.command.infer.options.maxOutgoingTransitionsOption
 import ru.ifmo.fbsat.cli.command.infer.options.numberOfModulesOption
 import ru.ifmo.fbsat.cli.command.infer.options.outDirOption
 import ru.ifmo.fbsat.cli.command.infer.options.outputNamesOption
@@ -35,6 +36,7 @@ private class ParallelModularBasicMinCAutomatonOptions : OptionGroup(AUTOMATON_O
     val numberOfModules: Int by numberOfModulesOption().required()
     val startNumberOfStates: Int by startNumberOfStatesOption().default(1)
     val endNumberOfStates: Int by endNumberOfStatesOption().default(20)
+    val maxOutgoingTransitions: Int? by maxOutgoingTransitionsOption()
 }
 
 class InferParallelModularBasicMinCCommand :
@@ -55,6 +57,7 @@ class InferParallelModularBasicMinCCommand :
             scenarioTree = scenarioTree,
             numberOfModules = params.numberOfModules,
             start = params.startNumberOfStates,
-            end = params.endNumberOfStates
+            end = params.endNumberOfStates,
+            maxOutgoingTransitionsForC = { params.maxOutgoingTransitions ?: it }
         )
 }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
index b24cd9e0..c6f24048 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
@@ -54,6 +54,7 @@ fun Inferrer.parallelModularBasicMinC(
     numberOfModules: Int, // M
     start: Int = 1, // C_start
     end: Int = 20, // C_end
+    maxOutgoingTransitionsForC: (Int) -> Int = { it }, // lambda for computing K, input arg is C, K=C by default
 ): ParallelModularAutomaton {
     var best: ParallelModularAutomaton? = null
     for (C in start..end) {
@@ -61,7 +62,8 @@ fun Inferrer.parallelModularBasicMinC(
             parallelModularBasic(
                 scenarioTree = scenarioTree,
                 numberOfModules = numberOfModules,
-                numberOfStates = C
+                numberOfStates = C,
+                maxOutgoingTransitions = maxOutgoingTransitionsForC(C)
             )
         }
         if (result != null) {
@@ -80,8 +82,14 @@ fun Inferrer.parallelModularBasicMin(
     scenarioTree: PositiveScenarioTree,
     numberOfModules: Int, // M
     numberOfStates: Int? = null, // C_start, 1 if null
+    maxOutgoingTransitionsForC: (Int) -> Int = { it }, // lambda for computing K, input arg is C, K=C by default
 ): ParallelModularAutomaton? {
-    parallelModularBasicMinC(scenarioTree, numberOfModules = numberOfModules, start = numberOfStates ?: 1)
+    parallelModularBasicMinC(
+        scenarioTree,
+        numberOfModules = numberOfModules,
+        start = numberOfStates ?: 1,
+        maxOutgoingTransitionsForC = maxOutgoingTransitionsForC
+    )
     return if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
         optimizeParallelModularA()
     } else {

From 95c82ad9a20d0552c7ffb287eda6e2b8bc25b086 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Sun, 24 Oct 2021 19:19:27 +0300
Subject: [PATCH 21/32] Share active[v] between all parallel modules

---
 .../basic/parallel/ParallelModularBasicVariables.kt  | 12 +++++++++++-
 .../fbsat/core/task/single/basic/BasicVariables.kt   |  6 ++++--
 2 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
index 5ce58b99..71f1fff9 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
@@ -1,5 +1,6 @@
 package ru.ifmo.fbsat.core.task.modular.basic.parallel
 
+import com.github.lipen.multiarray.IntMultiArray
 import com.github.lipen.satlib.card.declareCardinality
 import com.github.lipen.satlib.core.BoolVarArray
 import com.github.lipen.satlib.core.IntVarArray
@@ -43,12 +44,21 @@ fun Solver.declareParallelModularBasicVariables(
 
     /* Modular */
     declareModularContext(M)
-    forEachModularContext {
+    var active: IntMultiArray? = null
+    forEachModularContext { m ->
+        if (m != 1) {
+            logger.debug("Reusing active[v] for module m = $m")
+            context("active") { active!! }
+        }
         declareBasicVariables(
             positiveScenarioTree = scenarioTree,
             C = C, K = K,
             V = V, E = E, O = O, X = X, Z = Z, U = U
         )
+        if (m == 1) {
+            logger.debug("Saving active[v] from module m = $m")
+            active = context["active"]
+        }
     }
 
     /* Interface variables */
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
index 4568f2e3..182a45a1 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
@@ -117,8 +117,10 @@ fun Solver.declareBasicVariables(
         newIntVarArray(V) { 1..C }
     }
     if (Globals.IS_ENCODE_EVENTLESS) {
-        val active = context("active") {
-            newBoolVarArray(V)
+        if (!context.map.containsKey("active")) {
+            val active = context("active") {
+                newBoolVarArray(V)
+            }
         }
     }
 

From 7c9fead5f5bdabbd0a362e787ba8632fbd7686a0 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 25 Oct 2021 17:08:16 +0300
Subject: [PATCH 22/32] Add eventless modular parallel reduction

---
 .../automaton/ParallelModularAutomaton.kt     |   6 +
 .../core/constraints/MappingConstraints.kt    | 292 +++++++++++++++---
 .../parallel/ParallelModularBasicVariables.kt |  19 +-
 .../core/task/single/basic/BasicVariables.kt  |   3 +-
 4 files changed, 264 insertions(+), 56 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
index 087a9e34..a67ebf5a 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
@@ -30,6 +30,7 @@ import ru.ifmo.fbsat.core.utils.ModularContext
 import ru.ifmo.fbsat.core.utils.MyLogger
 import ru.ifmo.fbsat.core.utils.mutableListOfNulls
 import ru.ifmo.fbsat.core.utils.random
+import ru.ifmo.fbsat.core.utils.toBinaryString
 import ru.ifmo.fbsat.core.utils.withIndex
 import ru.ifmo.fbsat.core.utils.writeEventMerger
 import java.io.File
@@ -331,6 +332,11 @@ fun buildBasicParallelModularAutomaton(
     val modularContext: ModularContext = context["modularContext"]
     val moduleControllingOutputVariable = context.convertIntVarArray("moduleControllingOutputVariable", model)
 
+    if (Globals.IS_ENCODE_EVENTLESS) {
+        val active = context.convertBoolVarArray("active", model)
+        logger.info("active = $active")
+    }
+
     val modules = modularContext.mapIndexed { (m), ctx ->
         val C: Int = ctx["C"]
         val K: Int = ctx["K"]
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
index 0631f80d..99863249 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
@@ -19,6 +19,7 @@ import com.github.lipen.satlib.op.implyIff
 import com.github.lipen.satlib.op.implyIffAnd
 import com.github.lipen.satlib.op.implyIffIte
 import com.github.lipen.satlib.op.implyImply
+import com.github.lipen.satlib.op.implyImplyIff
 import com.github.lipen.satlib.op.implyImplyImply
 import com.github.lipen.satlib.op.implyImplyOr
 import com.github.lipen.satlib.op.implyOr
@@ -29,7 +30,9 @@ import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
 import ru.ifmo.fbsat.core.solver.autoneg
 import ru.ifmo.fbsat.core.solver.clause
 import ru.ifmo.fbsat.core.solver.forEachModularContext
+import ru.ifmo.fbsat.core.solver.imply2
 import ru.ifmo.fbsat.core.task.modular.basic.arbitrary.Pins
+import ru.ifmo.fbsat.core.utils.Globals
 import ru.ifmo.fbsat.core.utils.MyLogger
 import ru.ifmo.fbsat.core.utils.algorithmChoice
 import ru.ifmo.fbsat.core.utils.exhaustive
@@ -114,14 +117,14 @@ fun Solver.declareNegativeMappingConstraints(
     /* Constraints for active vertices */
     comment("Negative mapping constraints: for active nodes")
     for (v in Vs.intersect(negativeScenarioTree.activeVertices)) {
-        // comment("Negative mapping constraints: for active node v = $v")
+        // comment("Negative mapping constraints: for active node v = $v".also{logger.debug(it)
         declareMappingConstraintsForActiveNode(v = v, isPositive = false)
     }
 
     /* Constraints for passive vertices */
     comment("Negative mapping constraints: for passive nodes")
     for (v in Vs.intersect(negativeScenarioTree.passiveVertices)) {
-        // comment("Negative mapping constraints: for passive node v = $v")
+        // comment("Negative mapping constraints: for passive node v = $v".also{logger.debug(it)
         declareMappingConstraintsForPassiveNode(v = v, isPositive = false)
     }
 
@@ -164,57 +167,252 @@ fun Solver.declarePositiveParallelModularMappingConstraints(
     // Note: yet we only consider the SYNC-ALL mapping semantics
     val moduleControllingOutputVariable: IntVarArray = context["moduleControllingOutputVariable"]
 
-    forEachModularContext { m ->
-        val scenarioTree: PositiveScenarioTree = context["scenarioTree"]
-
-        /* Constraints for the root */
-        comment("Positive parallel modular mapping constraints: for root, module m = $m")
-        declareMappingConstraintsForRoot(isPositive = true)
-
-        /* Constraints for active vertices */
-        for (v in scenarioTree.activeVertices) {
-            comment("Positive parallel modular mapping constraints: for active node v = $v, module m = $m")
-            declareParallelModularMappingConstraintsForActiveNode(
-                m = m, v = v,
-                moduleControllingOutputVariable = moduleControllingOutputVariable
-            )
-        }
-
-        /* Constraints for passive vertices */
-        for (v in scenarioTree.passiveVertices) {
-            comment("Positive parallel modular mapping constraints: for passive node v = $v, module m = $m")
-            declareMappingConstraintsForPassiveNode(v = v, isPositive = true)
-        }
-
-        /* Additional constraints */
+    if (Globals.IS_ENCODE_EVENTLESS) {
+        forEachModularContext { m ->
+            comment("Eventless parallel modular positive mapping constraints")
 
-        if (isEncodeReverseImplication) {
-            comment("Mysterious reverse-implication: for module m = $m")
-            // OR_k(transitionDestination[i,k,j]) => OR_{v|active}( mapping[tp(v),i] & mapping[v,j] )
+            val tree: ScenarioTree<*, *> = context["tree"]
+            val V: Int = context["V"]
             val C: Int = context["C"]
             val K: Int = context["K"]
+            val E: Int = context["E"]
+            val Z: Int = context["Z"]
+            val U: Int = context["U"]
+            val stateOutputEvent: IntVarArray = context["stateOutputEvent"]
+            val stateAlgorithmTop: BoolVarArray = context["stateAlgorithmTop"]
+            val stateAlgorithmBot: BoolVarArray = context["stateAlgorithmBot"]
+            val actualTransitionFunction: IntVarArray = context["actualTransitionFunction"]
             val transitionDestination: IntVarArray = context["transitionDestination"]
             val mapping: IntVarArray = context["mapping"]
-            for (i in 1..C)
-                for (j in 1..C) {
-                    val lhsAux = newLiteral()
-                    iffOr(lhsAux) {
-                        for (k in 1..K)
-                            yield(transitionDestination[i, k] eq j)
+            val active: BoolVarArray = context["active"]
+
+            comment("Root maps to the first state")
+            clause(mapping[1] eq 1)
+
+            comment("Root is passive")
+            clause(-active[1])
+
+            comment("Mapping constraints")
+            for (v in 2..V) {
+                val p = tree.parent(v)
+                val e = tree.inputEvent(v)
+                val u = tree.inputNumber(v)
+                val o = tree.outputEvent(v)
+
+                // If any output value changed, then the node is definitely active
+                if ((1..Z).any { z -> tree.outputValue(v, z) != tree.outputValue(p, z) }) {
+                    clause(active[v])
+                }
+
+                if (Globals.IS_ENCODE_EPSILON_PASSIVE) {
+                    // If output event is epsilon, then the node is definitely passive
+                    if (o == 0) {
+                        clause(-active[v])
                     }
+                }
 
-                    val rhsAux = newLiteral()
-                    iffOr(rhsAux) {
-                        for (v in scenarioTree.activeVertices) {
-                            val p = scenarioTree.parent(v)
-                            val aux = newLiteral()
-                            iffAnd(aux, mapping[p] eq i, mapping[v] eq j)
-                            yield(aux)
-                        }
+                if (Globals.IS_ENCODE_NOT_EPSILON_ACTIVE) {
+                    // If output event is not epsilon, then the node is definitely active
+                    if (o != 0) {
+                        clause(active[v])
                     }
+                }
 
-                    imply(lhsAux, rhsAux)
+                if (Globals.IS_ENCODE_TRANSITION_FUNCTION) {
+                    val transitionFunction: IntVarArray = context["transitionFunction"]
+
+                    comment("Positive mapping/transitionFunction definition for v = $v")
+                    // (mapping[p] = q) => ((mapping[v] = q') <=> (transitionFunction[q,e,u] = q'))
+                    for (i in 1..C)
+                        for (j in 1..C)
+                            implyIff(
+                                mapping[p] eq i,
+                                mapping[v] eq j,
+                                transitionFunction[i, e, u] eq j
+                            )
                 }
+
+                comment("Positive active-mapping definition for v = $v")
+                // active[v] =>
+                //  (mapping[v] = c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)] = c)
+                for (i in 1..C)
+                    for (j in 1..C)
+                        implyImplyIff(
+                            active[v],
+                            mapping[p] eq i,
+                            mapping[v] eq j,
+                            actualTransitionFunction[i, e, u] eq j
+                        )
+                // active[v] =>
+                //  (mapping[v] = c) => (stateOutputEvent[c] = toe(v))
+                for (c in 1..C)
+                    imply2(
+                        active[v],
+                        mapping[v] eq c,
+                        stateOutputEvent[c] eq o
+                    )
+                // active[v] =>
+                //  (mapping[v] = c) => AND_{z}(moduleControllingOutputVariable[z]=m) => (stateAlgorithm{tov(tp(v),z)}[c,z] = tov(v,z)))
+                for (c in 1..C)
+                    for (z in 1..Z)
+                        implyImplyImply(
+                            active[v],
+                            mapping[v] eq c,
+                            moduleControllingOutputVariable[z] eq m,
+                            algorithmChoice(
+                                tree = tree,
+                                v = v, c = c, z = z,
+                                algorithmTop = stateAlgorithmTop,
+                                algorithmBot = stateAlgorithmBot
+                            )
+                        )
+
+                comment("REVERSE actualTransitionFunction/active")
+                // (mapping[p] = q) & (actualTransitionFunction[q,e,u] != 0) => active[v]
+                for (c in 1..C)
+                    imply2(
+                        mapping[p] eq c,
+                        actualTransitionFunction[c, e, u] neq 0,
+                        active[v]
+                    )
+
+                comment("Positive passive-mapping definition for v = $v")
+                // ~active[v] =>
+                //  mapping[v] = mapping[tp(v)]
+                for (c in 1..C)
+                    imply2(
+                        -active[v],
+                        mapping[p] eq c,
+                        mapping[v] eq c
+                    )
+                // ~active[v] =>
+                //  (mapping[tp(v)] = c) => (actualTransition[c,tie(v),tin(v)] = 0)
+                for (c in 1..C)
+                    imply2(
+                        -active[v],
+                        mapping[p] eq c,
+                        actualTransitionFunction[c, e, u] eq 0
+                    )
+
+                comment("REVERSE actualTransitionFunction/passive")
+                // (mapping[p] = q) & (actualTransitionFunction[q,e,u] = 0) => ~active[v]
+                for (c in 1..C)
+                    imply2(
+                        mapping[p] eq c,
+                        actualTransitionFunction[c, e, u] eq 0,
+                        -active[v]
+                    )
+
+                // comment("Parallel modular mapping definition for active node v = $v, module m = $m")
+                // (mapping[v]=c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)]=c) & (stateOutputEvent[c]=toe(v)) & AND_{z}( (moduleControllingOutputVariable[z]=m) => (stateAlgorithm{tov(tp(v),z)}(c,z) = tov(v,z)) )
+                // for (i in 1..C)
+                //     for (j in 1..C)
+                //         implyIffAnd(
+                //             mapping[p] eq i,
+                //             mapping[v] eq j
+                //         ) {
+                //             yield(actualTransitionFunction[i, e, u] eq j)
+                //             yield(stateOutputEvent[j] eq o)
+                //             for (z in 1..Z)
+                //                 yield(
+                //                     newLiteral().also { aux ->
+                //                         iffImply(
+                //                             aux,
+                //                             moduleControllingOutputVariable[z] eq m,
+                //                             algorithmChoice(
+                //                                 tree = tree,
+                //                                 v = v, c = j, z = z,
+                //                                 algorithmTop = stateAlgorithmTop,
+                //                                 algorithmBot = stateAlgorithmBot
+                //                             )
+                //                         )
+                //                     }
+                //                 )
+                //         }
+            }
+
+            if (isEncodeReverseImplication) {
+                comment("Mysterious reverse-implication")
+                // OR_k(transitionDestination[i,k,j]) => OR_{v}( mapping[p]=i & mapping[v]=j & active[v] )
+                for (i in 1..C)
+                    for (j in 1..C) {
+                        val lhsAux = newLiteral()
+                        iffOr(lhsAux) {
+                            for (k in 1..K)
+                                yield(transitionDestination[i, k] eq j)
+                        }
+
+                        // val rhsAux = newLiteral()
+                        val rhsAux = lhsAux // Note: when encoding `<=>` it is better to just use the same literal
+                        iffOr(rhsAux) {
+                            for (v in 2..V) {
+                                val p = tree.parent(v)
+                                val aux = newLiteral()
+                                iffAnd(aux, mapping[p] eq i, mapping[v] eq j, active[v])
+                                yield(aux)
+                            }
+                        }
+
+                        // imply(lhsAux, rhsAux)
+                        //
+                        // // Adhoc: other way around!
+                        // imply(rhsAux, lhsAux)
+                    }
+            }
+        }
+    } else {
+        forEachModularContext { m ->
+            val scenarioTree: PositiveScenarioTree = context["scenarioTree"]
+
+            /* Constraints for the root */
+            comment("Positive parallel modular mapping constraints: for root, module m = $m")
+            declareMappingConstraintsForRoot(isPositive = true)
+
+            /* Constraints for active vertices */
+            for (v in scenarioTree.activeVertices) {
+                comment("Positive parallel modular mapping constraints: for active node v = $v, module m = $m")
+                declareParallelModularMappingConstraintsForActiveNode(
+                    m = m, v = v,
+                    moduleControllingOutputVariable = moduleControllingOutputVariable
+                )
+            }
+
+            /* Constraints for passive vertices */
+            for (v in scenarioTree.passiveVertices) {
+                comment("Positive parallel modular mapping constraints: for passive node v = $v, module m = $m")
+                declareMappingConstraintsForPassiveNode(v = v, isPositive = true)
+            }
+
+            /* Additional constraints */
+
+            if (isEncodeReverseImplication) {
+                comment("Mysterious reverse-implication: for module m = $m")
+                // OR_k(transitionDestination[i,k,j]) => OR_{v|active}( mapping[tp(v),i] & mapping[v,j] )
+                val C: Int = context["C"]
+                val K: Int = context["K"]
+                val transitionDestination: IntVarArray = context["transitionDestination"]
+                val mapping: IntVarArray = context["mapping"]
+                for (i in 1..C)
+                    for (j in 1..C) {
+                        val lhsAux = newLiteral()
+                        iffOr(lhsAux) {
+                            for (k in 1..K)
+                                yield(transitionDestination[i, k] eq j)
+                        }
+
+                        val rhsAux = newLiteral()
+                        iffOr(rhsAux) {
+                            for (v in scenarioTree.activeVertices) {
+                                val p = scenarioTree.parent(v)
+                                val aux = newLiteral()
+                                iffAnd(aux, mapping[p] eq i, mapping[v] eq j)
+                                yield(aux)
+                            }
+                        }
+
+                        imply(lhsAux, rhsAux)
+                    }
+            }
         }
     }
 }
@@ -410,10 +608,10 @@ fun Solver.declarePositiveArbitraryModularMappingConstraints(
 fun Solver.declareDistributedPositiveMappingConstraints_modular(
     modularIsEncodeReverseImplication: MultiArray<Boolean>,
 ) {
-    // comment("Distributed positive mapping constraints")
+    // comment("Distributed positive mapping constraints".also{logger.debug(it)
     // with(distributedBasicVariables) {
     //     for (m in 1..M) {
-    //         comment("Distributed positive mapping constraints: module m = $m")
+    //         comment("Distributed positive mapping constraints: module m = $m".also{logger.debug(it)
     //         declarePositiveMappingConstraints(
     //             basicVariables = modularBasicVariables[m],
     //             isEncodeReverseImplication = modularIsEncodeReverseImplication[m]
@@ -643,7 +841,7 @@ private fun Solver.declareArbitraryModularMappingConstraintsForActiveNode(
     val stateAlgorithmTop: BoolVarArray = context["stateAlgorithmTop"]
     val mapping: IntVarArray = context["mapping"]
 
-    // comment("Arbitrary modular mapping definition for active node v = $v, module m = $m")
+    // comment("Arbitrary modular mapping definition for active node v = $v, module m = $m".also{logger.debug(it)
 
     // (inputIndex[v]=u) => (mapping[tp(v)]=i) => (mapping[v]=j) <=> (actualTransition[i,u]=j))
     // Note: implyImplyImply vs implyImplyIff
@@ -797,7 +995,7 @@ private fun Solver.declareMappingConstraintsForActiveNode(
                     )
                 )
     } else {
-        // comment("Negative mapping definition for active node v = $v")
+        // comment("Negative mapping definition for active node v = $v".also{logger.debug(it)
         // // (mapping[v]=c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)]=c) & (stateOutputEvent[c]=toe(v)) & AND_{z}(stateAlgorithm{tov(tp(v),z)}[c,z] = tov(v,z))
         // for (i in 1..C)
         //     for (j in 1..C)
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
index 71f1fff9..1a2e2345 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt
@@ -1,10 +1,10 @@
 package ru.ifmo.fbsat.core.task.modular.basic.parallel
 
-import com.github.lipen.multiarray.IntMultiArray
 import com.github.lipen.satlib.card.declareCardinality
 import com.github.lipen.satlib.core.BoolVarArray
 import com.github.lipen.satlib.core.IntVarArray
 import com.github.lipen.satlib.core.neq
+import com.github.lipen.satlib.core.newBoolVarArray
 import com.github.lipen.satlib.core.newIntVarArray
 import com.github.lipen.satlib.solver.Solver
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
@@ -42,23 +42,26 @@ fun Solver.declareParallelModularBasicVariables(
     context["Z"] = Z
     context["U"] = U
 
+    val active = if (Globals.IS_ENCODE_EVENTLESS) {
+        context("active") {
+            newBoolVarArray(V)
+        }
+    } else {
+        null
+    }
+
     /* Modular */
     declareModularContext(M)
-    var active: IntMultiArray? = null
     forEachModularContext { m ->
-        if (m != 1) {
+        if (Globals.IS_ENCODE_EVENTLESS) {
             logger.debug("Reusing active[v] for module m = $m")
-            context("active") { active!! }
+            context["active"] = active!!
         }
         declareBasicVariables(
             positiveScenarioTree = scenarioTree,
             C = C, K = K,
             V = V, E = E, O = O, X = X, Z = Z, U = U
         )
-        if (m == 1) {
-            logger.debug("Saving active[v] from module m = $m")
-            active = context["active"]
-        }
     }
 
     /* Interface variables */
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
index 182a45a1..54f6bb70 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
@@ -8,7 +8,7 @@ import com.github.lipen.satlib.core.neq
 import com.github.lipen.satlib.core.newBoolVarArray
 import com.github.lipen.satlib.core.newIntVar
 import com.github.lipen.satlib.core.newIntVarArray
-import com.github.lipen.satlib.op.iffAnd
+import com.github.lipen.satlib.op.*
 import com.github.lipen.satlib.solver.Solver
 import ru.ifmo.fbsat.core.scenario.initialOutputValues
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
@@ -118,6 +118,7 @@ fun Solver.declareBasicVariables(
     }
     if (Globals.IS_ENCODE_EVENTLESS) {
         if (!context.map.containsKey("active")) {
+            logger.debug("Declaring 'active'")
             val active = context("active") {
                 newBoolVarArray(V)
             }

From c30e213463350b7dbb77262bb43024c529c02341 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 25 Oct 2021 17:09:22 +0300
Subject: [PATCH 23/32] Comment logging

---
 .../ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
index a67ebf5a..b24a5f9c 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
@@ -332,10 +332,10 @@ fun buildBasicParallelModularAutomaton(
     val modularContext: ModularContext = context["modularContext"]
     val moduleControllingOutputVariable = context.convertIntVarArray("moduleControllingOutputVariable", model)
 
-    if (Globals.IS_ENCODE_EVENTLESS) {
-        val active = context.convertBoolVarArray("active", model)
-        logger.info("active = $active")
-    }
+    // if (Globals.IS_ENCODE_EVENTLESS) {
+    //     val active = context.convertBoolVarArray("active", model)
+    //     logger.info("active = $active")
+    // }
 
     val modules = modularContext.mapIndexed { (m), ctx ->
         val C: Int = ctx["C"]

From 3485af7162cf41a96eaf99389bfafe1ce679bbaf Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 25 Oct 2021 17:19:50 +0300
Subject: [PATCH 24/32] Remove unnecessary import

---
 .../ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt     | 1 -
 1 file changed, 1 deletion(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
index b24a5f9c..902c3334 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
@@ -30,7 +30,6 @@ import ru.ifmo.fbsat.core.utils.ModularContext
 import ru.ifmo.fbsat.core.utils.MyLogger
 import ru.ifmo.fbsat.core.utils.mutableListOfNulls
 import ru.ifmo.fbsat.core.utils.random
-import ru.ifmo.fbsat.core.utils.toBinaryString
 import ru.ifmo.fbsat.core.utils.withIndex
 import ru.ifmo.fbsat.core.utils.writeEventMerger
 import java.io.File

From d61b93e8a94120fd68e10d7ad7d51d43a841f939 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 26 Oct 2021 15:47:50 +0300
Subject: [PATCH 25/32] Extract eventless parallel modular mapping

---
 .../EventlessMappingConstraints.kt            | 173 +++++++++++
 .../core/constraints/MappingConstraints.kt    | 282 +++---------------
 .../parallel/ParallelModularBasicTask.kt      |   7 +-
 .../core/task/single/basic/BasicVariables.kt  |   1 -
 4 files changed, 222 insertions(+), 241 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt
index f35ff2c2..31b33efe 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt
@@ -9,9 +9,11 @@ import com.github.lipen.satlib.op.iffOr
 import com.github.lipen.satlib.op.imply
 import com.github.lipen.satlib.op.implyIff
 import com.github.lipen.satlib.op.implyImplyIff
+import com.github.lipen.satlib.op.implyImplyImply
 import com.github.lipen.satlib.solver.Solver
 import ru.ifmo.fbsat.core.scenario.ScenarioTree
 import ru.ifmo.fbsat.core.solver.clause
+import ru.ifmo.fbsat.core.solver.forEachModularContext
 import ru.ifmo.fbsat.core.solver.imply2
 import ru.ifmo.fbsat.core.utils.Globals
 import ru.ifmo.fbsat.core.utils.algorithmChoice
@@ -237,3 +239,174 @@ fun Solver.declareEventlessPositiveMappingConstraints(
             }
     }
 }
+
+fun Solver.declareEventlessPositiveParallelModularMappingConstraints(
+    isEncodeReverseImplication: Boolean,
+) {
+    comment("Eventless parallel modular positive mapping constraints")
+    // Note: yet we only consider the SYNC-ALL mapping semantics
+    val moduleControllingOutputVariable: IntVarArray = context["moduleControllingOutputVariable"]
+
+    forEachModularContext { m ->
+        val tree: ScenarioTree<*, *> = context["tree"]
+        val V: Int = context["V"]
+        val C: Int = context["C"]
+        val K: Int = context["K"]
+        val Z: Int = context["Z"]
+        val stateOutputEvent: IntVarArray = context["stateOutputEvent"]
+        val stateAlgorithmTop: BoolVarArray = context["stateAlgorithmTop"]
+        val stateAlgorithmBot: BoolVarArray = context["stateAlgorithmBot"]
+        val actualTransitionFunction: IntVarArray = context["actualTransitionFunction"]
+        val transitionDestination: IntVarArray = context["transitionDestination"]
+        val mapping: IntVarArray = context["mapping"]
+        val active: BoolVarArray = context["active"]
+
+        comment("Root maps to the first state")
+        clause(mapping[1] eq 1)
+
+        comment("Root is passive")
+        clause(-active[1])
+
+        comment("Mapping constraints")
+        for (v in 2..V) {
+            val p = tree.parent(v)
+            val e = tree.inputEvent(v)
+            val u = tree.inputNumber(v)
+            val o = tree.outputEvent(v)
+
+            // If any output value changed, then the node is definitely active
+            if ((1..Z).any { z -> tree.outputValue(v, z) != tree.outputValue(p, z) }) {
+                clause(active[v])
+            }
+
+            if (Globals.IS_ENCODE_EPSILON_PASSIVE) {
+                // If output event is epsilon, then the node is definitely passive
+                if (o == 0) {
+                    clause(-active[v])
+                }
+            }
+
+            if (Globals.IS_ENCODE_NOT_EPSILON_ACTIVE) {
+                // If output event is not epsilon, then the node is definitely active
+                if (o != 0) {
+                    clause(active[v])
+                }
+            }
+
+            if (Globals.IS_ENCODE_TRANSITION_FUNCTION) {
+                val transitionFunction: IntVarArray = context["transitionFunction"]
+
+                comment("Positive mapping/transitionFunction definition for v = $v")
+                // (mapping[p] = q) => ((mapping[v] = q') <=> (transitionFunction[q,e,u] = q'))
+                for (i in 1..C)
+                    for (j in 1..C)
+                        implyIff(
+                            mapping[p] eq i,
+                            mapping[v] eq j,
+                            transitionFunction[i, e, u] eq j
+                        )
+            }
+
+            comment("Positive active-mapping definition for v = $v")
+            // active[v] =>
+            //  (mapping[v] = c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)] = c)
+            for (i in 1..C)
+                for (j in 1..C)
+                    implyImplyIff(
+                        active[v],
+                        mapping[p] eq i,
+                        mapping[v] eq j,
+                        actualTransitionFunction[i, e, u] eq j
+                    )
+            // active[v] =>
+            //  (mapping[v] = c) => (stateOutputEvent[c] = toe(v))
+            for (c in 1..C)
+                imply2(
+                    active[v],
+                    mapping[v] eq c,
+                    stateOutputEvent[c] eq o
+                )
+            // active[v] =>
+            //  (mapping[v] = c) => AND_{z}(moduleControllingOutputVariable[z]=m) => (stateAlgorithm{tov(tp(v),z)}[c,z] = tov(v,z)))
+            // Note: here we use `moduleControllingOutputVariable`, because we are inside parallel-modular reduction
+            for (c in 1..C)
+                for (z in 1..Z)
+                    implyImplyImply(
+                        active[v],
+                        mapping[v] eq c,
+                        moduleControllingOutputVariable[z] eq m,
+                        algorithmChoice(
+                            tree = tree,
+                            v = v, c = c, z = z,
+                            algorithmTop = stateAlgorithmTop,
+                            algorithmBot = stateAlgorithmBot
+                        )
+                    )
+
+            comment("REVERSE actualTransitionFunction/active")
+            // (mapping[p] = q) & (actualTransitionFunction[q,e,u] != 0) => active[v]
+            for (c in 1..C)
+                imply2(
+                    mapping[p] eq c,
+                    actualTransitionFunction[c, e, u] neq 0,
+                    active[v]
+                )
+
+            comment("Positive passive-mapping definition for v = $v")
+            // ~active[v] =>
+            //  mapping[v] = mapping[tp(v)]
+            for (c in 1..C)
+                imply2(
+                    -active[v],
+                    mapping[p] eq c,
+                    mapping[v] eq c
+                )
+            // ~active[v] =>
+            //  (mapping[tp(v)] = c) => (actualTransition[c,tie(v),tin(v)] = 0)
+            for (c in 1..C)
+                imply2(
+                    -active[v],
+                    mapping[p] eq c,
+                    actualTransitionFunction[c, e, u] eq 0
+                )
+
+            comment("REVERSE actualTransitionFunction/passive")
+            // (mapping[p] = q) & (actualTransitionFunction[q,e,u] = 0) => ~active[v]
+            for (c in 1..C)
+                imply2(
+                    mapping[p] eq c,
+                    actualTransitionFunction[c, e, u] eq 0,
+                    -active[v]
+                )
+        }
+
+        if (isEncodeReverseImplication) {
+            comment("Mysterious reverse-implication")
+            // OR_k(transitionDestination[i,k,j]) => OR_{v}( mapping[p]=i & mapping[v]=j & active[v] )
+            for (i in 1..C)
+                for (j in 1..C) {
+                    val lhsAux = newLiteral()
+                    iffOr(lhsAux) {
+                        for (k in 1..K)
+                            yield(transitionDestination[i, k] eq j)
+                    }
+
+                    // val rhsAux = newLiteral()
+                    val rhsAux = lhsAux // Note: when encoding `<=>` it is better to just use the same literal
+                    iffOr(rhsAux) {
+                        for (v in 2..V) {
+                            val p = tree.parent(v)
+                            val aux = newLiteral()
+                            iffAnd(aux, mapping[p] eq i, mapping[v] eq j, active[v])
+                            yield(aux)
+                        }
+                    }
+
+                    // imply(lhsAux, rhsAux)
+                    //
+                    // // Adhoc: other way around!
+                    // imply(rhsAux, lhsAux)
+                }
+        }
+    }
+}
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
index 99863249..46f28b0b 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
@@ -19,7 +19,6 @@ import com.github.lipen.satlib.op.implyIff
 import com.github.lipen.satlib.op.implyIffAnd
 import com.github.lipen.satlib.op.implyIffIte
 import com.github.lipen.satlib.op.implyImply
-import com.github.lipen.satlib.op.implyImplyIff
 import com.github.lipen.satlib.op.implyImplyImply
 import com.github.lipen.satlib.op.implyImplyOr
 import com.github.lipen.satlib.op.implyOr
@@ -30,9 +29,7 @@ import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
 import ru.ifmo.fbsat.core.solver.autoneg
 import ru.ifmo.fbsat.core.solver.clause
 import ru.ifmo.fbsat.core.solver.forEachModularContext
-import ru.ifmo.fbsat.core.solver.imply2
 import ru.ifmo.fbsat.core.task.modular.basic.arbitrary.Pins
-import ru.ifmo.fbsat.core.utils.Globals
 import ru.ifmo.fbsat.core.utils.MyLogger
 import ru.ifmo.fbsat.core.utils.algorithmChoice
 import ru.ifmo.fbsat.core.utils.exhaustive
@@ -167,252 +164,59 @@ fun Solver.declarePositiveParallelModularMappingConstraints(
     // Note: yet we only consider the SYNC-ALL mapping semantics
     val moduleControllingOutputVariable: IntVarArray = context["moduleControllingOutputVariable"]
 
-    if (Globals.IS_ENCODE_EVENTLESS) {
-        forEachModularContext { m ->
-            comment("Eventless parallel modular positive mapping constraints")
-
-            val tree: ScenarioTree<*, *> = context["tree"]
-            val V: Int = context["V"]
-            val C: Int = context["C"]
-            val K: Int = context["K"]
-            val E: Int = context["E"]
-            val Z: Int = context["Z"]
-            val U: Int = context["U"]
-            val stateOutputEvent: IntVarArray = context["stateOutputEvent"]
-            val stateAlgorithmTop: BoolVarArray = context["stateAlgorithmTop"]
-            val stateAlgorithmBot: BoolVarArray = context["stateAlgorithmBot"]
-            val actualTransitionFunction: IntVarArray = context["actualTransitionFunction"]
-            val transitionDestination: IntVarArray = context["transitionDestination"]
-            val mapping: IntVarArray = context["mapping"]
-            val active: BoolVarArray = context["active"]
-
-            comment("Root maps to the first state")
-            clause(mapping[1] eq 1)
+    forEachModularContext { m ->
+        val scenarioTree: PositiveScenarioTree = context["scenarioTree"]
 
-            comment("Root is passive")
-            clause(-active[1])
+        /* Constraints for the root */
+        comment("Positive parallel modular mapping constraints: for root, module m = $m")
+        declareMappingConstraintsForRoot(isPositive = true)
 
-            comment("Mapping constraints")
-            for (v in 2..V) {
-                val p = tree.parent(v)
-                val e = tree.inputEvent(v)
-                val u = tree.inputNumber(v)
-                val o = tree.outputEvent(v)
+        /* Constraints for active vertices */
+        for (v in scenarioTree.activeVertices) {
+            comment("Positive parallel modular mapping constraints: for active node v = $v, module m = $m")
+            declareParallelModularMappingConstraintsForActiveNode(
+                m = m, v = v,
+                moduleControllingOutputVariable = moduleControllingOutputVariable
+            )
+        }
 
-                // If any output value changed, then the node is definitely active
-                if ((1..Z).any { z -> tree.outputValue(v, z) != tree.outputValue(p, z) }) {
-                    clause(active[v])
-                }
+        /* Constraints for passive vertices */
+        for (v in scenarioTree.passiveVertices) {
+            comment("Positive parallel modular mapping constraints: for passive node v = $v, module m = $m")
+            declareMappingConstraintsForPassiveNode(v = v, isPositive = true)
+        }
 
-                if (Globals.IS_ENCODE_EPSILON_PASSIVE) {
-                    // If output event is epsilon, then the node is definitely passive
-                    if (o == 0) {
-                        clause(-active[v])
-                    }
-                }
+        /* Additional constraints */
 
-                if (Globals.IS_ENCODE_NOT_EPSILON_ACTIVE) {
-                    // If output event is not epsilon, then the node is definitely active
-                    if (o != 0) {
-                        clause(active[v])
+        if (isEncodeReverseImplication) {
+            comment("Mysterious reverse-implication: for module m = $m")
+            // OR_k(transitionDestination[i,k,j]) => OR_{v|active}( mapping[tp(v),i] & mapping[v,j] )
+            val C: Int = context["C"]
+            val K: Int = context["K"]
+            val transitionDestination: IntVarArray = context["transitionDestination"]
+            val mapping: IntVarArray = context["mapping"]
+            for (i in 1..C)
+                for (j in 1..C) {
+                    val lhsAux = newLiteral()
+                    iffOr(lhsAux) {
+                        for (k in 1..K)
+                            yield(transitionDestination[i, k] eq j)
                     }
-                }
-
-                if (Globals.IS_ENCODE_TRANSITION_FUNCTION) {
-                    val transitionFunction: IntVarArray = context["transitionFunction"]
-
-                    comment("Positive mapping/transitionFunction definition for v = $v")
-                    // (mapping[p] = q) => ((mapping[v] = q') <=> (transitionFunction[q,e,u] = q'))
-                    for (i in 1..C)
-                        for (j in 1..C)
-                            implyIff(
-                                mapping[p] eq i,
-                                mapping[v] eq j,
-                                transitionFunction[i, e, u] eq j
-                            )
-                }
-
-                comment("Positive active-mapping definition for v = $v")
-                // active[v] =>
-                //  (mapping[v] = c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)] = c)
-                for (i in 1..C)
-                    for (j in 1..C)
-                        implyImplyIff(
-                            active[v],
-                            mapping[p] eq i,
-                            mapping[v] eq j,
-                            actualTransitionFunction[i, e, u] eq j
-                        )
-                // active[v] =>
-                //  (mapping[v] = c) => (stateOutputEvent[c] = toe(v))
-                for (c in 1..C)
-                    imply2(
-                        active[v],
-                        mapping[v] eq c,
-                        stateOutputEvent[c] eq o
-                    )
-                // active[v] =>
-                //  (mapping[v] = c) => AND_{z}(moduleControllingOutputVariable[z]=m) => (stateAlgorithm{tov(tp(v),z)}[c,z] = tov(v,z)))
-                for (c in 1..C)
-                    for (z in 1..Z)
-                        implyImplyImply(
-                            active[v],
-                            mapping[v] eq c,
-                            moduleControllingOutputVariable[z] eq m,
-                            algorithmChoice(
-                                tree = tree,
-                                v = v, c = c, z = z,
-                                algorithmTop = stateAlgorithmTop,
-                                algorithmBot = stateAlgorithmBot
-                            )
-                        )
-
-                comment("REVERSE actualTransitionFunction/active")
-                // (mapping[p] = q) & (actualTransitionFunction[q,e,u] != 0) => active[v]
-                for (c in 1..C)
-                    imply2(
-                        mapping[p] eq c,
-                        actualTransitionFunction[c, e, u] neq 0,
-                        active[v]
-                    )
-
-                comment("Positive passive-mapping definition for v = $v")
-                // ~active[v] =>
-                //  mapping[v] = mapping[tp(v)]
-                for (c in 1..C)
-                    imply2(
-                        -active[v],
-                        mapping[p] eq c,
-                        mapping[v] eq c
-                    )
-                // ~active[v] =>
-                //  (mapping[tp(v)] = c) => (actualTransition[c,tie(v),tin(v)] = 0)
-                for (c in 1..C)
-                    imply2(
-                        -active[v],
-                        mapping[p] eq c,
-                        actualTransitionFunction[c, e, u] eq 0
-                    )
 
-                comment("REVERSE actualTransitionFunction/passive")
-                // (mapping[p] = q) & (actualTransitionFunction[q,e,u] = 0) => ~active[v]
-                for (c in 1..C)
-                    imply2(
-                        mapping[p] eq c,
-                        actualTransitionFunction[c, e, u] eq 0,
-                        -active[v]
-                    )
-
-                // comment("Parallel modular mapping definition for active node v = $v, module m = $m")
-                // (mapping[v]=c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)]=c) & (stateOutputEvent[c]=toe(v)) & AND_{z}( (moduleControllingOutputVariable[z]=m) => (stateAlgorithm{tov(tp(v),z)}(c,z) = tov(v,z)) )
-                // for (i in 1..C)
-                //     for (j in 1..C)
-                //         implyIffAnd(
-                //             mapping[p] eq i,
-                //             mapping[v] eq j
-                //         ) {
-                //             yield(actualTransitionFunction[i, e, u] eq j)
-                //             yield(stateOutputEvent[j] eq o)
-                //             for (z in 1..Z)
-                //                 yield(
-                //                     newLiteral().also { aux ->
-                //                         iffImply(
-                //                             aux,
-                //                             moduleControllingOutputVariable[z] eq m,
-                //                             algorithmChoice(
-                //                                 tree = tree,
-                //                                 v = v, c = j, z = z,
-                //                                 algorithmTop = stateAlgorithmTop,
-                //                                 algorithmBot = stateAlgorithmBot
-                //                             )
-                //                         )
-                //                     }
-                //                 )
-                //         }
-            }
-
-            if (isEncodeReverseImplication) {
-                comment("Mysterious reverse-implication")
-                // OR_k(transitionDestination[i,k,j]) => OR_{v}( mapping[p]=i & mapping[v]=j & active[v] )
-                for (i in 1..C)
-                    for (j in 1..C) {
-                        val lhsAux = newLiteral()
-                        iffOr(lhsAux) {
-                            for (k in 1..K)
-                                yield(transitionDestination[i, k] eq j)
-                        }
-
-                        // val rhsAux = newLiteral()
-                        val rhsAux = lhsAux // Note: when encoding `<=>` it is better to just use the same literal
-                        iffOr(rhsAux) {
-                            for (v in 2..V) {
-                                val p = tree.parent(v)
-                                val aux = newLiteral()
-                                iffAnd(aux, mapping[p] eq i, mapping[v] eq j, active[v])
-                                yield(aux)
-                            }
+                    // val rhsAux = newLiteral()
+                    val rhsAux = lhsAux // Note: when encoding `<=>` it is better to just use the same literal
+                    iffOr(rhsAux) {
+                        for (v in scenarioTree.activeVertices) {
+                            val p = scenarioTree.parent(v)
+                            val aux = newLiteral()
+                            iffAnd(aux, mapping[p] eq i, mapping[v] eq j)
+                            yield(aux)
                         }
-
-                        // imply(lhsAux, rhsAux)
-                        //
-                        // // Adhoc: other way around!
-                        // imply(rhsAux, lhsAux)
                     }
-            }
-        }
-    } else {
-        forEachModularContext { m ->
-            val scenarioTree: PositiveScenarioTree = context["scenarioTree"]
-
-            /* Constraints for the root */
-            comment("Positive parallel modular mapping constraints: for root, module m = $m")
-            declareMappingConstraintsForRoot(isPositive = true)
-
-            /* Constraints for active vertices */
-            for (v in scenarioTree.activeVertices) {
-                comment("Positive parallel modular mapping constraints: for active node v = $v, module m = $m")
-                declareParallelModularMappingConstraintsForActiveNode(
-                    m = m, v = v,
-                    moduleControllingOutputVariable = moduleControllingOutputVariable
-                )
-            }
 
-            /* Constraints for passive vertices */
-            for (v in scenarioTree.passiveVertices) {
-                comment("Positive parallel modular mapping constraints: for passive node v = $v, module m = $m")
-                declareMappingConstraintsForPassiveNode(v = v, isPositive = true)
-            }
-
-            /* Additional constraints */
-
-            if (isEncodeReverseImplication) {
-                comment("Mysterious reverse-implication: for module m = $m")
-                // OR_k(transitionDestination[i,k,j]) => OR_{v|active}( mapping[tp(v),i] & mapping[v,j] )
-                val C: Int = context["C"]
-                val K: Int = context["K"]
-                val transitionDestination: IntVarArray = context["transitionDestination"]
-                val mapping: IntVarArray = context["mapping"]
-                for (i in 1..C)
-                    for (j in 1..C) {
-                        val lhsAux = newLiteral()
-                        iffOr(lhsAux) {
-                            for (k in 1..K)
-                                yield(transitionDestination[i, k] eq j)
-                        }
-
-                        val rhsAux = newLiteral()
-                        iffOr(rhsAux) {
-                            for (v in scenarioTree.activeVertices) {
-                                val p = scenarioTree.parent(v)
-                                val aux = newLiteral()
-                                iffAnd(aux, mapping[p] eq i, mapping[v] eq j)
-                                yield(aux)
-                            }
-                        }
-
-                        imply(lhsAux, rhsAux)
-                    }
-            }
+                    // imply(lhsAux, rhsAux)
+                    // imply(rhsAux, lhsAux)
+                }
         }
     }
 }
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt
index c79ca956..051d0bad 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt
@@ -2,6 +2,7 @@ package ru.ifmo.fbsat.core.task.modular.basic.parallel
 
 import com.github.lipen.satlib.card.Cardinality
 import com.github.lipen.satlib.solver.Solver
+import ru.ifmo.fbsat.core.constraints.declareEventlessPositiveParallelModularMappingConstraints
 import ru.ifmo.fbsat.core.constraints.declareParallelModularAutomatonBfsConstraints
 import ru.ifmo.fbsat.core.constraints.declareParallelModularAutomatonStructureConstraints
 import ru.ifmo.fbsat.core.constraints.declarePositiveParallelModularMappingConstraints
@@ -31,7 +32,11 @@ data class ParallelModularBasicTask(
         comment("$name: Constraints")
         declareParallelModularAutomatonStructureConstraints()
         if (Globals.IS_BFS_AUTOMATON) declareParallelModularAutomatonBfsConstraints()
-        declarePositiveParallelModularMappingConstraints(isEncodeReverseImplication)
+        if (Globals.IS_ENCODE_EVENTLESS) {
+            declareEventlessPositiveParallelModularMappingConstraints(isEncodeReverseImplication)
+        } else {
+            declarePositiveParallelModularMappingConstraints(isEncodeReverseImplication)
+        }
 
         /* Initial cardinality constraints */
         comment("$name: Initial cardinality (T) constraints")
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
index 54f6bb70..7ba95bf1 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt
@@ -118,7 +118,6 @@ fun Solver.declareBasicVariables(
     }
     if (Globals.IS_ENCODE_EVENTLESS) {
         if (!context.map.containsKey("active")) {
-            logger.debug("Declaring 'active'")
             val active = context("active") {
                 newBoolVarArray(V)
             }

From 6dcb5447f177fb0ecb3de3f4464fd530760cf9e6 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 26 Oct 2021 15:50:44 +0300
Subject: [PATCH 26/32] Rename

---
 .../fbsat/core/constraints/EventlessMappingConstraints.kt     | 2 +-
 .../task/modular/basic/parallel/ParallelModularBasicTask.kt   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt
index 31b33efe..d91f5291 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt
@@ -240,7 +240,7 @@ fun Solver.declareEventlessPositiveMappingConstraints(
     }
 }
 
-fun Solver.declareEventlessPositiveParallelModularMappingConstraints(
+fun Solver.declarePositiveParallelModularEventlessMappingConstraints(
     isEncodeReverseImplication: Boolean,
 ) {
     comment("Eventless parallel modular positive mapping constraints")
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt
index 051d0bad..1ff9e504 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt
@@ -2,7 +2,7 @@ package ru.ifmo.fbsat.core.task.modular.basic.parallel
 
 import com.github.lipen.satlib.card.Cardinality
 import com.github.lipen.satlib.solver.Solver
-import ru.ifmo.fbsat.core.constraints.declareEventlessPositiveParallelModularMappingConstraints
+import ru.ifmo.fbsat.core.constraints.declarePositiveParallelModularEventlessMappingConstraints
 import ru.ifmo.fbsat.core.constraints.declareParallelModularAutomatonBfsConstraints
 import ru.ifmo.fbsat.core.constraints.declareParallelModularAutomatonStructureConstraints
 import ru.ifmo.fbsat.core.constraints.declarePositiveParallelModularMappingConstraints
@@ -33,7 +33,7 @@ data class ParallelModularBasicTask(
         declareParallelModularAutomatonStructureConstraints()
         if (Globals.IS_BFS_AUTOMATON) declareParallelModularAutomatonBfsConstraints()
         if (Globals.IS_ENCODE_EVENTLESS) {
-            declareEventlessPositiveParallelModularMappingConstraints(isEncodeReverseImplication)
+            declarePositiveParallelModularEventlessMappingConstraints(isEncodeReverseImplication)
         } else {
             declarePositiveParallelModularMappingConstraints(isEncodeReverseImplication)
         }

From a2af700a162c2ebd7309afe923bf58e0d0c59622 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 26 Oct 2021 16:27:28 +0300
Subject: [PATCH 27/32] Fix verification (simulation check) of eventless
 scenarios

---
 .../core/automaton/ParallelModularAutomaton.kt    | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
index 902c3334..494850e1 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
@@ -19,6 +19,7 @@ import ru.ifmo.fbsat.core.scenario.OutputAction
 import ru.ifmo.fbsat.core.scenario.OutputEvent
 import ru.ifmo.fbsat.core.scenario.OutputValues
 import ru.ifmo.fbsat.core.scenario.Scenario
+import ru.ifmo.fbsat.core.scenario.outputValues
 import ru.ifmo.fbsat.core.scenario.positive.OldPositiveScenarioTree
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenario
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
@@ -108,10 +109,18 @@ class ParallelModularAutomaton(
             check(result.values.mapNotNull { it.outputAction.event }.all { it == outputEvent })
             val outputValues = gather(MultiArray.new(M) { (m) -> result[m].outputAction.values })
 
-            if (OutputAction(outputEvent, outputValues) == element.outputAction) {
-                results[j] = result
+            if (Globals.IS_ENCODE_EVENTLESS) {
+                if (outputValues == element.outputValues) {
+                    results[j] = result
+                } else {
+                    break
+                }
             } else {
-                break
+                if (OutputAction(outputEvent, outputValues) == element.outputAction) {
+                    results[j] = result
+                } else {
+                    break
+                }
             }
 
             for (m in 1..M) {

From 2ef335de174620fae648916d1fbf3820b412c7be Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 26 Oct 2021 16:28:35 +0300
Subject: [PATCH 28/32] Adopt eventless mapping for distributed synthesis

---
 .../EventlessMappingConstraints.kt            | 179 ++++++++++++++++++
 .../distributed/basic/DistributedBasicTask.kt |   9 +-
 2 files changed, 186 insertions(+), 2 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt
index d91f5291..8d91e99c 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt
@@ -1,5 +1,6 @@
 package ru.ifmo.fbsat.core.constraints
 
+import com.github.lipen.multiarray.MultiArray
 import com.github.lipen.satlib.core.BoolVarArray
 import com.github.lipen.satlib.core.IntVarArray
 import com.github.lipen.satlib.core.eq
@@ -8,6 +9,7 @@ import com.github.lipen.satlib.op.iffAnd
 import com.github.lipen.satlib.op.iffOr
 import com.github.lipen.satlib.op.imply
 import com.github.lipen.satlib.op.implyIff
+import com.github.lipen.satlib.op.implyImply
 import com.github.lipen.satlib.op.implyImplyIff
 import com.github.lipen.satlib.op.implyImplyImply
 import com.github.lipen.satlib.solver.Solver
@@ -410,3 +412,180 @@ fun Solver.declarePositiveParallelModularEventlessMappingConstraints(
         }
     }
 }
+
+fun Solver.declareDistributedPositiveEventlessMappingConstraints_compound(
+    modularIsEncodeReverseImplication: MultiArray<Boolean>,
+) {
+    comment("Distributed [COMPOUND] positive eventless mapping constraints")
+
+    forEachModularContext { m ->
+        comment("Distributed [COMPOUND] positive eventless mapping constraints: for module m = $m")
+
+        val tree: ScenarioTree<*, *> = context["tree"]
+        val V: Int = context["V"]
+        val C: Int = context["C"]
+        val K: Int = context["K"]
+        val Z: Int = context["Z"]
+        val stateOutputEvent: IntVarArray = context["stateOutputEvent"]
+        val stateAlgorithmTop: BoolVarArray = context["stateAlgorithmTop"]
+        val stateAlgorithmBot: BoolVarArray = context["stateAlgorithmBot"]
+        val actualTransitionFunction: IntVarArray = context["actualTransitionFunction"]
+        val transitionDestination: IntVarArray = context["transitionDestination"]
+        val mapping: IntVarArray = context["mapping"]
+        val active: BoolVarArray = context["active"]
+        val stateUsed: BoolVarArray = context["stateUsed"]
+
+        comment("Root maps to the first state")
+        clause(mapping[1] eq 1)
+
+        comment("Root is passive")
+        clause(-active[1])
+
+        comment("Mapping constraints")
+        for (v in 2..V) {
+            val p = tree.parent(v)
+            val e = tree.inputEvent(v)
+            val u = tree.inputNumber(v)
+            val o = tree.outputEvent(v)
+
+            // If any output value changed, then the node is definitely active
+            if ((1..Z).any { z -> tree.outputValue(v, z) != tree.outputValue(p, z) }) {
+                clause(active[v])
+            }
+
+            if (Globals.IS_ENCODE_EPSILON_PASSIVE) {
+                // If output event is epsilon, then the node is definitely passive
+                if (o == 0) {
+                    clause(-active[v])
+                }
+            }
+
+            if (Globals.IS_ENCODE_NOT_EPSILON_ACTIVE) {
+                // If output event is not epsilon, then the node is definitely active
+                if (o != 0) {
+                    clause(active[v])
+                }
+            }
+
+            if (Globals.IS_ENCODE_TRANSITION_FUNCTION) {
+                val transitionFunction: IntVarArray = context["transitionFunction"]
+
+                comment("Positive mapping/transitionFunction definition for v = $v")
+                // (mapping[p] = q) => ((mapping[v] = q') <=> (transitionFunction[q,e,u] = q'))
+                for (i in 1..C)
+                    for (j in 1..C)
+                        implyIff(
+                            mapping[p] eq i,
+                            mapping[v] eq j,
+                            transitionFunction[i, e, u] eq j
+                        )
+            }
+
+            comment("Positive active-mapping definition for v = $v")
+            // active[v] =>
+            //  (mapping[v] = c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)] = c)
+            for (i in 1..C)
+                for (j in 1..C)
+                    implyImplyIff(
+                        active[v],
+                        mapping[p] eq i,
+                        mapping[v] eq j,
+                        actualTransitionFunction[i, e, u] eq j
+                    )
+            // active[v] =>
+            //  (mapping[v] = c) => (stateOutputEvent[c] = toe(v))
+            for (c in 1..C)
+                imply2(
+                    active[v],
+                    mapping[v] eq c,
+                    stateOutputEvent[c] eq o
+                )
+            // active[v] =>
+            //  (mapping[v] = c) => AND_{z}(stateAlgorithm{tov(tp(v),z)}[c,z] = tov(v,z))
+            for (c in 1..C)
+                for (z in 1..Z)
+                    implyImply(
+                        active[v],
+                        mapping[v] eq c,
+                        algorithmChoice(
+                            tree = tree,
+                            v = v, c = c, z = z,
+                            algorithmTop = stateAlgorithmTop,
+                            algorithmBot = stateAlgorithmBot
+                        )
+                    )
+
+            comment("REVERSE actualTransitionFunction/active")
+            // (mapping[p] = q) & (actualTransitionFunction[q,e,u] != 0) => active[v]
+            for (c in 1..C)
+                imply2(
+                    mapping[p] eq c,
+                    actualTransitionFunction[c, e, u] neq 0,
+                    active[v]
+                )
+
+            comment("Positive passive-mapping definition for v = $v")
+            // ~active[v] =>
+            //  mapping[v] = mapping[tp(v)]
+            for (c in 1..C)
+                imply2(
+                    -active[v],
+                    mapping[p] eq c,
+                    mapping[v] eq c
+                )
+            // ~active[v] =>
+            //  (mapping[tp(v)] = c) => (actualTransition[c,tie(v),tin(v)] = 0)
+            for (c in 1..C)
+                imply2(
+                    -active[v],
+                    mapping[p] eq c,
+                    actualTransitionFunction[c, e, u] eq 0
+                )
+
+            comment("REVERSE actualTransitionFunction/passive")
+            // (mapping[p] = q) & (actualTransitionFunction[q,e,u] = 0) => ~active[v]
+            for (c in 1..C)
+                imply2(
+                    mapping[p] eq c,
+                    actualTransitionFunction[c, e, u] eq 0,
+                    -active[v]
+                )
+        }
+
+        /* Constraints for all vertices */
+        for (v in 1..V)
+            for (c in 1..C)
+                imply(
+                    -stateUsed[c],
+                    mapping[v] neq c
+                )
+
+        val isEncodeReverseImplication = modularIsEncodeReverseImplication[m]
+        if (isEncodeReverseImplication) {
+            comment("Mysterious reverse-implication")
+            // OR_k(transitionDestination[i,k,j]) => OR_{v}( mapping[p]=i & mapping[v]=j & active[v] )
+            for (i in 1..C)
+                for (j in 1..C) {
+                    val lhsAux = newLiteral()
+                    iffOr(lhsAux) {
+                        for (k in 1..K)
+                            yield(transitionDestination[i, k] eq j)
+                    }
+
+                    // val rhsAux = newLiteral()
+                    val rhsAux = lhsAux // Note: when encoding `<=>` it is better to just use the same literal
+                    iffOr(rhsAux) {
+                        for (v in 2..V) {
+                            val p = tree.parent(v)
+                            val aux = newLiteral()
+                            iffAnd(aux, mapping[p] eq i, mapping[v] eq j, active[v])
+                            yield(aux)
+                        }
+                    }
+
+                    // imply(lhsAux, rhsAux)
+                    // imply(rhsAux, lhsAux)
+                }
+        }
+    }
+}
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/distributed/basic/DistributedBasicTask.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/distributed/basic/DistributedBasicTask.kt
index e376d58b..3ef445d5 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/distributed/basic/DistributedBasicTask.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/distributed/basic/DistributedBasicTask.kt
@@ -6,6 +6,7 @@ import com.github.lipen.satlib.card.Cardinality
 import com.github.lipen.satlib.solver.Solver
 import ru.ifmo.fbsat.core.constraints.declareDistributedAutomatonBfsConstraints
 import ru.ifmo.fbsat.core.constraints.declareDistributedAutomatonStructureConstraints
+import ru.ifmo.fbsat.core.constraints.declareDistributedPositiveEventlessMappingConstraints_compound
 import ru.ifmo.fbsat.core.constraints.declareDistributedPositiveMappingConstraints_compound
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
 import ru.ifmo.fbsat.core.solver.forEachModularContext
@@ -48,8 +49,12 @@ data class DistributedBasicTask(
         comment("$name: Constraints")
         declareDistributedAutomatonStructureConstraints()
         if (Globals.IS_BFS_AUTOMATON) declareDistributedAutomatonBfsConstraints()
-        // declareDistributedPositiveMappingConstraints_modular(vars, modularIsEncodeReverseImplication)
-        declareDistributedPositiveMappingConstraints_compound(modularIsEncodeReverseImplication)
+        if (Globals.IS_ENCODE_EVENTLESS) {
+            declareDistributedPositiveEventlessMappingConstraints_compound(modularIsEncodeReverseImplication)
+        } else {
+            // declareDistributedPositiveMappingConstraints_modular(vars, modularIsEncodeReverseImplication)
+            declareDistributedPositiveMappingConstraints_compound(modularIsEncodeReverseImplication)
+        }
         // declareDistributedBasicAdhocConstraints()
 
         /* Initial cardinality constraints */

From a46d297904b85a555e947d960d31e31702323d0b Mon Sep 17 00:00:00 2001
From: Daniil Chivilikhin <chivdan@itmo.ru>
Date: Tue, 26 Oct 2021 13:54:13 +0000
Subject: [PATCH 29/32] Added logging of input/output decompositions and active
 variables. Added option to fix active variables

---
 .../cli/command/infer/AbstractInferCommand.kt |  1 +
 .../cli/command/infer/options/ExtraOptions.kt | 15 +++++-
 .../automaton/ParallelModularAutomaton.kt     | 28 ++++++----
 .../AutomatonStructureConstraints.kt          | 26 +++++++++
 .../core/constraints/MappingConstraints.kt    | 53 ++++++++++---------
 .../basic/parallel/ParallelModularBasic.kt    |  8 ++-
 .../ru/ifmo/fbsat/core/utils/Globals.kt       |  1 +
 7 files changed, 95 insertions(+), 37 deletions(-)

diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
index 2da3a237..bec96153 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt
@@ -25,6 +25,7 @@ abstract class AbstractInferCommand<AutomatonType : Any>(name: String) : CliktCo
             Globals.EPSILON_OUTPUT_EVENTS = epsilonOutputEvents
             Globals.START_STATE_ALGORITHMS = startStateAlgorithms
             Globals.FIXED_OUTPUT_DECOMPOSITION = fixedOutputDecomposition
+            Globals.FIXED_ACTIVITY = fixedActivity
             Globals.IS_FORBID_OR = isForbidOr
             Globals.IS_FORBID_TRANSITIONS_TO_FIRST_STATE = isForbidTransitionsToFirstState
             Globals.IS_BFS_AUTOMATON = isBfsAutomaton
diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
index 16c74545..a40bf7f9 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
@@ -25,6 +25,7 @@ class ExtraOptions : OptionGroup(EXTRA_OPTIONS) {
     val epsilonOutputEvents: EpsilonOutputEvents by getEpsilonOutputEventsOption()
     val startStateAlgorithms: StartStateAlgorithms by getStartStateAlgorithmsOption()
     val fixedOutputDecomposition: List<Int?>? by getFixedOutputDecompositionOption()
+    val fixedActivity: List<Boolean?>? by getFixedActivityOption()
     val isEncodeReverseImplication: Boolean by isEncodeReverseImplicationOption()
     val isEncodeTransitionsOrder: Boolean by isEncodeTransitionsOrderOption()
     val isEncodeTerminalsOrder: Boolean by isEncodeTerminalsOrderOption()
@@ -129,10 +130,22 @@ fun ParameterHolder.getFixedOutputDecompositionOption() =
     ).convert {
         require(it.isNotBlank()) { "string should not be blank" }
         it.split(",").map { s ->
-            s.trim().toIntOrNull()
+            s.trim().toInt()
         }
     }
 
+fun ParameterHolder.getFixedActivityOption() =
+    option(
+        "--fixed-activity",
+        help = "[modular-parallel] Comma-separated values of activity of scenario tree elements"
+    ).convert {
+        require(it.isNotBlank()) { "string should not be blank" }
+        it.split(",").map { s ->
+            s.trim().toBooleanStrictOrNull()
+        }
+    }
+
+
 fun ParameterHolder.isEncodeReverseImplicationOption() =
     option(
         "--encode-reverse-implication",
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
index 902c3334..cd87c23a 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt
@@ -19,6 +19,7 @@ import ru.ifmo.fbsat.core.scenario.OutputAction
 import ru.ifmo.fbsat.core.scenario.OutputEvent
 import ru.ifmo.fbsat.core.scenario.OutputValues
 import ru.ifmo.fbsat.core.scenario.Scenario
+import ru.ifmo.fbsat.core.scenario.outputValues
 import ru.ifmo.fbsat.core.scenario.positive.OldPositiveScenarioTree
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenario
 import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree
@@ -60,6 +61,7 @@ class ParallelModularAutomaton(
     val numberOfStates: Int = modules.values.sumOf { it.numberOfStates }
     val numberOfTransitions: Int = modules.values.sumOf { it.numberOfTransitions }
     val totalGuardsSize: Int = modules.values.sumOf { it.totalGuardsSize }
+//    val numberOfActiveVertices = sumOf {it.active}
 
     init {
         require(modules.values.all { it.inputEvents == inputEvents })
@@ -108,11 +110,19 @@ class ParallelModularAutomaton(
             check(result.values.mapNotNull { it.outputAction.event }.all { it == outputEvent })
             val outputValues = gather(MultiArray.new(M) { (m) -> result[m].outputAction.values })
 
-            if (OutputAction(outputEvent, outputValues) == element.outputAction) {
-                results[j] = result
-            } else {
-                break
-            }
+	    if (!Globals.IS_ENCODE_EVENTLESS) {
+		if (OutputAction(outputEvent, outputValues) == element.outputAction) {
+		    results[j] = result
+		} else {
+		    break
+		}
+	    } else {
+		if (outputValues == element.outputValues) {
+		    results[j] = result
+		} else {
+	            break
+		}
+	    }
 
             for (m in 1..M) {
                 currentState[m] = result[m].destination
@@ -331,10 +341,10 @@ fun buildBasicParallelModularAutomaton(
     val modularContext: ModularContext = context["modularContext"]
     val moduleControllingOutputVariable = context.convertIntVarArray("moduleControllingOutputVariable", model)
 
-    // if (Globals.IS_ENCODE_EVENTLESS) {
-    //     val active = context.convertBoolVarArray("active", model)
-    //     logger.info("active = $active")
-    // }
+    if (Globals.IS_ENCODE_EVENTLESS) {
+        val active = context.convertBoolVarArray("active", model)
+        logger.info("active = $active")
+    }
 
     val modules = modularContext.mapIndexed { (m), ctx ->
         val C: Int = ctx["C"]
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
index 000dc609..8bf5d726 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt
@@ -55,6 +55,7 @@ fun Solver.declareNegativeAutomatonStructureConstraints(Us: Iterable<Int>) {
 
 fun Solver.declareParallelModularAutomatonStructureConstraints() {
     comment("Parallel modular automaton structure constraints")
+    val V: Int = context["V"]
     val M: Int = context["M"]
     val Z: Int = context["Z"]
     val moduleControllingOutputVariable: IntVarArray = context["moduleControllingOutputVariable"]
@@ -101,6 +102,31 @@ fun Solver.declareParallelModularAutomatonStructureConstraints() {
             }
         }
     }
+
+    forEachModularContext { m ->
+        comment("Parallel modular automaton structure constraints: for module m = $m")
+    }
+
+    if (Globals.FIXED_ACTIVITY != null) {
+        comment("(adhoc) Fixing scenario tree node activity")
+        val activeValues: List<Boolean?> = Globals.FIXED_ACTIVITY!!
+
+	forEachModularContext { m ->
+ 	    comment("Parallel modular automaton structure constraints: for module m = $m")
+	    val active: BoolVarArray = context["active"]
+	    for (v in 1..V) { 
+		if (activeValues[v - 1] == null) {
+		    continue
+                }
+		if (activeValues[v - 1]!!) {
+	            clause(active[v])
+                } else {
+	            clause(-active[v])
+	        }
+            }
+	}
+    }
+
 }
 
 fun Solver.declareConsecutiveModularAutomatonStructureConstraints() {
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
index 99863249..6fcb8312 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
@@ -16,6 +16,7 @@ import com.github.lipen.satlib.op.iffImply
 import com.github.lipen.satlib.op.iffOr
 import com.github.lipen.satlib.op.imply
 import com.github.lipen.satlib.op.implyIff
+import com.github.lipen.satlib.op.implyImplyIffAnd
 import com.github.lipen.satlib.op.implyIffAnd
 import com.github.lipen.satlib.op.implyIffIte
 import com.github.lipen.satlib.op.implyImply
@@ -303,32 +304,34 @@ fun Solver.declarePositiveParallelModularMappingConstraints(
                         -active[v]
                     )
 
-                // comment("Parallel modular mapping definition for active node v = $v, module m = $m")
+                 comment("Parallel modular mapping definition for active node v = $v, module m = $m")
                 // (mapping[v]=c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)]=c) & (stateOutputEvent[c]=toe(v)) & AND_{z}( (moduleControllingOutputVariable[z]=m) => (stateAlgorithm{tov(tp(v),z)}(c,z) = tov(v,z)) )
-                // for (i in 1..C)
-                //     for (j in 1..C)
-                //         implyIffAnd(
-                //             mapping[p] eq i,
-                //             mapping[v] eq j
-                //         ) {
-                //             yield(actualTransitionFunction[i, e, u] eq j)
-                //             yield(stateOutputEvent[j] eq o)
-                //             for (z in 1..Z)
-                //                 yield(
-                //                     newLiteral().also { aux ->
-                //                         iffImply(
-                //                             aux,
-                //                             moduleControllingOutputVariable[z] eq m,
-                //                             algorithmChoice(
-                //                                 tree = tree,
-                //                                 v = v, c = j, z = z,
-                //                                 algorithmTop = stateAlgorithmTop,
-                //                                 algorithmBot = stateAlgorithmBot
-                //                             )
-                //                         )
-                //                     }
-                //                 )
-                //         }
+/*                 for (i in 1..C)
+                     for (j in 1..C)
+                         implyImplyIffAnd(
+		             active[v],
+                             mapping[p] eq i,
+                             mapping[v] eq j
+                         ) {
+                             yield(actualTransitionFunction[i, e, u] eq j)
+                             yield(stateOutputEvent[j] eq o)
+                             for (z in 1..Z)
+                                 yield(
+                                     newLiteral().also { aux ->
+                                         iffImply(
+                                             aux,
+                                             moduleControllingOutputVariable[z] eq m,
+                                             algorithmChoice(
+                                                 tree = tree,
+                                                 v = v, c = j, z = z,
+                                                 algorithmTop = stateAlgorithmTop,
+                                                 algorithmBot = stateAlgorithmBot
+                                             )
+                                         )
+                                     }
+                                 )
+                         }
+			 */
             }
 
             if (isEncodeReverseImplication) {
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
index c6f24048..2a17f767 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
@@ -100,16 +100,20 @@ fun Inferrer.parallelModularBasicMin(
 fun Inferrer.inferParallelModularBasic(): ParallelModularAutomaton? {
     val model = solveAndGetModel() ?: return null
     val automaton = buildBasicParallelModularAutomaton(solver.context, model)
+    val moduleControllingOutputVariable =
+    solver.context.convertIntVarArray("moduleControllingOutputVariable", model)
+
+    logger.info("output-decomposition = " + moduleControllingOutputVariable)
 
     if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) {
         val modularContext: ModularContext = solver.context["modularContext"]
-        val moduleControllingOutputVariable =
-            solver.context.convertIntVarArray("moduleControllingOutputVariable", model)
         modularContext.forEachIndexed { (m), ctx ->
             val scenarioTree: PositiveScenarioTree = ctx["scenarioTree"]
             val X: Int = ctx["X"]
             val Z: Int = ctx["Z"]
             val inputVariableUsed = ctx.convertBoolVarArray("inputVariableUsed", model)
+            logger.info("$m: input-used = $inputVariableUsed")
+
 
             val sliceInput = (1..X).filter { x ->
                 inputVariableUsed[x]
diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
index eecef830..583c86d2 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt
@@ -16,6 +16,7 @@ object Globals {
     var EPSILON_OUTPUT_EVENTS: EpsilonOutputEvents = EpsilonOutputEvents.ONLYSTART
     var START_STATE_ALGORITHMS: StartStateAlgorithms = StartStateAlgorithms.ZERO
     var FIXED_OUTPUT_DECOMPOSITION: List<Int?>? = null
+    var FIXED_ACTIVITY: List<Boolean?>? = null
     var IS_FORBID_OR: Boolean = false
     var IS_FORBID_TRANSITIONS_TO_FIRST_STATE: Boolean = true
     var IS_BFS_AUTOMATON: Boolean = true

From 03d43d942b63312c88b4495b32f2937305c6ea13 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 26 Oct 2021 17:12:04 +0300
Subject: [PATCH 30/32] Fix help

---
 .../ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt  | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
index a40bf7f9..9de10d80 100644
--- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
+++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt
@@ -137,15 +137,14 @@ fun ParameterHolder.getFixedOutputDecompositionOption() =
 fun ParameterHolder.getFixedActivityOption() =
     option(
         "--fixed-activity",
-        help = "[modular-parallel] Comma-separated values of activity of scenario tree elements"
+        help = "[modular-parallel] Comma-separated values (boolean) of activity of scenario tree elements"
     ).convert {
         require(it.isNotBlank()) { "string should not be blank" }
         it.split(",").map { s ->
-            s.trim().toBooleanStrictOrNull()
+            s.trim().toBoolean()
         }
     }
 
-
 fun ParameterHolder.isEncodeReverseImplicationOption() =
     option(
         "--encode-reverse-implication",

From 6b0c74f86fee187c4f6ad90b9b830769bb55b9ee Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 26 Oct 2021 17:12:15 +0300
Subject: [PATCH 31/32] Fix formatting

---
 .../core/task/modular/basic/parallel/ParallelModularBasic.kt   | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
index 2a17f767..65de9830 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt
@@ -101,7 +101,7 @@ fun Inferrer.inferParallelModularBasic(): ParallelModularAutomaton? {
     val model = solveAndGetModel() ?: return null
     val automaton = buildBasicParallelModularAutomaton(solver.context, model)
     val moduleControllingOutputVariable =
-    solver.context.convertIntVarArray("moduleControllingOutputVariable", model)
+        solver.context.convertIntVarArray("moduleControllingOutputVariable", model)
 
     logger.info("output-decomposition = " + moduleControllingOutputVariable)
 
@@ -114,7 +114,6 @@ fun Inferrer.inferParallelModularBasic(): ParallelModularAutomaton? {
             val inputVariableUsed = ctx.convertBoolVarArray("inputVariableUsed", model)
             logger.info("$m: input-used = $inputVariableUsed")
 
-
             val sliceInput = (1..X).filter { x ->
                 inputVariableUsed[x]
             }.map { it - 1 }

From d97b22d75e3bf754c8579e5c50970057bc35366e Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 26 Oct 2021 17:14:03 +0300
Subject: [PATCH 32/32] Remove unnecessary import

---
 .../kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt  | 1 -
 1 file changed, 1 deletion(-)

diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
index d6db53a2..46f28b0b 100644
--- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
+++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt
@@ -16,7 +16,6 @@ import com.github.lipen.satlib.op.iffImply
 import com.github.lipen.satlib.op.iffOr
 import com.github.lipen.satlib.op.imply
 import com.github.lipen.satlib.op.implyIff
-import com.github.lipen.satlib.op.implyImplyIffAnd
 import com.github.lipen.satlib.op.implyIffAnd
 import com.github.lipen.satlib.op.implyIffIte
 import com.github.lipen.satlib.op.implyImply