Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

Implement input-vars decomposition for parallel modular synthesis#16

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to ourterms of service andprivacy statement. We’ll occasionally send you account related emails.

Already on GitHub?Sign in to your account

Open
Lipen wants to merge35 commits intomaster
base:master
Choose a base branch
Loading
fromfeature/input-decomposition
Open
Show file tree
Hide file tree
Changes from1 commit
Commits
Show all changes
35 commits
Select commitHold shift + click to select a range
4acd3f4
Implement input vars decomposition
LipenOct 17, 2021
872708d
Add ConjunctiveGuard to SerializersModule
LipenOct 17, 2021
264f7d0
Back-merge 'master'
LipenOct 17, 2021
b5336f8
Add dumping of sliced scenarios after modular-parallel-basic inferenc…
LipenOct 18, 2021
5681c21
Fix(adhoc) Guard::truthTableString calculation for TruthTableGuard
LipenOct 19, 2021
1cdd430
Back-merge 'master'
LipenOct 19, 2021
9d4ba76
Add missing imports of extension props
LipenOct 19, 2021
1ec38bf
Fix cardinality and optimization
LipenOct 19, 2021
1a7a5a8
Remove unnecessary comma
LipenOct 19, 2021
bfaa96c
Add --fixed-output-decomposition option
LipenOct 20, 2021
5d2752a
Remove unnecessary extension methods
LipenOct 20, 2021
f13f26d
Fix typo
LipenOct 20, 2021
6cf3ba5
Fix free variables
LipenOct 20, 2021
b7f6904
Remove UNNECESSARY constraint. Add ALO(used)
LipenOct 20, 2021
da0ab0d
Add logging of output decomposition
LipenOct 20, 2021
f4f1b61
Fix typo
LipenOct 20, 2021
843fd67
Add constraint for 0-guards on null-transitions
LipenOct 20, 2021
a50ecef
Add implication (tau!=0) to conjunctive guard definition
LipenOct 21, 2021
179fa33
Fix automaton mapping in eventless case
LipenOct 21, 2021
5a7bf44
Add some logging, cleanup
LipenOct 21, 2021
5e4ae84
Add stub for --fix-output-decomposition flag
LipenOct 21, 2021
c656408
Add maxOutgoingTransitions option for parallel-modular-basic tasks
LipenOct 21, 2021
95c82ad
Share active[v] between all parallel modules
LipenOct 24, 2021
7c9fead
Add eventless modular parallel reduction
LipenOct 25, 2021
c30e213
Comment logging
LipenOct 25, 2021
3485af7
Remove unnecessary import
LipenOct 25, 2021
d61b93e
Extract eventless parallel modular mapping
LipenOct 26, 2021
6dcb544
Rename
LipenOct 26, 2021
a2af700
Fix verification (simulation check) of eventless scenarios
LipenOct 26, 2021
2ef335d
Adopt eventless mapping for distributed synthesis
LipenOct 26, 2021
a46d297
Added logging of input/output decompositions and active variables. Ad…
Oct 26, 2021
8349bb9
Merge 'input-decomposition-daniil' into feature/input-decomposition
LipenOct 26, 2021
03d43d9
Fix help
LipenOct 26, 2021
6b0c74f
Fix formatting
LipenOct 26, 2021
d97b22d
Remove unnecessary import
LipenOct 26, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
PrevPrevious commit
NextNext commit
Add maxOutgoingTransitions option for parallel-modular-basic tasks
  • Loading branch information
@Lipen
Lipen committedOct 21, 2021
commitc65640854f23b4f46cb17aad3c7bf6cbd27cff2f
Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand All@@ -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 :
Expand All@@ -51,6 +53,7 @@ class InferParallelModularBasicMinCommand :
inferrer.parallelModularBasicMin(
scenarioTree = scenarioTree,
numberOfModules = params.numberOfModules,
numberOfStates = params.numberOfStates
numberOfStates = params.numberOfStates,
maxOutgoingTransitionsForC = { params.maxOutgoingTransitions ?: it }
)
}
Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand All@@ -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 :
Expand All@@ -55,6 +57,7 @@ class InferParallelModularBasicMinCCommand :
scenarioTree = scenarioTree,
numberOfModules = params.numberOfModules,
start = params.startNumberOfStates,
end = params.endNumberOfStates
end = params.endNumberOfStates,
maxOutgoingTransitionsForC = { params.maxOutgoingTransitions ?: it }
)
}
Original file line numberDiff line numberDiff line change
Expand Up@@ -54,14 +54,16 @@ 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) {
val (result, runningTime) = measureTimeWithResult {
parallelModularBasic(
scenarioTree = scenarioTree,
numberOfModules = numberOfModules,
numberOfStates = C
numberOfStates = C,
maxOutgoingTransitions = maxOutgoingTransitionsForC(C)
)
}
if (result != null) {
Expand All@@ -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 {
Expand Down
[8]ページ先頭
©2009-2025 Movatter.jp