Implement input-vars decomposition for parallel modular synthesis

fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt

@@ -24,6 +24,8 @@ 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.FIXED_ACTIVITY = fixedActivity
             Globals.IS_FORBID_OR = isForbidOr
             Globals.IS_FORBID_TRANSITIONS_TO_FIRST_STATE = isForbidTransitionsToFirstState
             Globals.IS_BFS_AUTOMATON = isBfsAutomaton
@@ -42,7 +44,10 @@ 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_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

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()))

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 }
         )
 }

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 }
         )
 }

fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt

@@ -24,6 +24,8 @@ 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 fixedActivity: List<Boolean?>? by getFixedActivityOption()
     val isEncodeReverseImplication: Boolean by isEncodeReverseImplicationOption()
     val isEncodeTransitionsOrder: Boolean by isEncodeTransitionsOrderOption()
     val isEncodeTerminalsOrder: Boolean by isEncodeTerminalsOrderOption()
@@ -38,7 +40,10 @@ 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 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()
@@ -118,6 +123,28 @@ 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().toInt()
+        }
+    }
+
+fun ParameterHolder.getFixedActivityOption() =
+    option(
+        "--fixed-activity",
+        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().toBoolean()
+        }
+    }
+
 fun ParameterHolder.isEncodeReverseImplicationOption() =
     option(
         "--encode-reverse-implication",
@@ -244,6 +271,24 @@ 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.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",
@@ -253,6 +298,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",

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
@@ -24,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
@@ -331,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
         }
@@ -530,11 +534,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 = ${getA()}}"
     }
 
     fun printStats() {
@@ -838,6 +843,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)
@@ -855,6 +861,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
@@ -879,15 +893,24 @@ 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) {
+                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
+                )
+            }
         }
     )
 }
@@ -962,3 +985,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
+}