Commit c61b7de7 authored by Anton Pirogov's avatar Anton Pirogov Committed by Anton Pirogov

Added new determinization construction (nbadet) and multiple simulations for NBA

parent 41990668
......@@ -21,6 +21,14 @@ src/**/gen/
*.iws
/out/
# ==== Eclipse files ====
.classpath
.project
.checkstyle
.factorypath
.settings
bin/
# ==== Python files ====
__pycache__/
......@@ -32,3 +40,5 @@ __pycache__/
*.so
*cmake-build-*
.DS_Store
/.apt_generated/
/.apt_generated_tests/
......@@ -197,6 +197,12 @@ NBA2DPA:
TEST_NAME: "nba2dpa"
<<: *ltlcross_template
NBADet:
stage: test
variables:
TEST_NAME: "nbadet"
<<: *ltlcross_template
## Conversions
DPA Conversion:
......
......@@ -10,10 +10,12 @@
* Christopher Ziegler
* Florian Barta
* Matthias Franze
* Anton Pirogov
* León Bohn
# Honorable mentions (previous versions)
* Andreas Gaiser
* Jan Kretinsky
* Zuzana Komarkova
* Ruslan Ledesma-Garza
\ No newline at end of file
* Ruslan Ledesma-Garza
......@@ -2,6 +2,17 @@
Modules:
* Added new general determinization construction for NBA based on papers
presented at ICALP'19 and ATVA'19. The construction supports multiple
optimizations and can be invoked using the `nbadet` tool.
* Added simulations for NBA: direct, delayed, fair and also
some other variants like with multi-pebble and lookahead simulations.
The tool `nbasim` can be used to preprocess an automaton by quotienting
states equivalent wrt. a suitable simulation.
* Added support for external parity game solver Oink.
* Added `ltl2normalform` that rewrites LTL formulas into the restricted
alternation normal form described in our LICS'20 submission.
......
......@@ -188,7 +188,11 @@ def scripts = [
'ltl2da' : 'owl.translations.modules.LTL2DAModule',
'ltl2na' : 'owl.translations.modules.LTL2NAModule',
// NBA -> DPA
'nbadet' : 'owl.translations.nbadet.NbaDet',
// Miscellaneous
'nbasim' : 'owl.automaton.algorithm.simulations.BuchiSimulation',
'nba2dpa' : 'owl.translations.nba2dpa.NBA2DPA',
'nba2ldba' : 'owl.translations.nba2ldba.NBA2LDBA',
'dra2dpa' : 'owl.translations.dra2dpa.IARBuilder',
......
......@@ -150,6 +150,40 @@
],
"data": "RANDOM"
},
"nbasim": {
"tools": [
"nbasim#refinement",
"nbasim#direct",
"nbasim#delayed"
],
"data": "L"
},
"nbadet": {
"tools": [
"nbadet#default"
],
"data": "L"
},
"nbadet-intense": {
"tools": [
"nbadet#mullerschupp",
"nbadet#mullerschupp,powersets",
"nbadet#mullerschupp,powersets,smartsucc",
"nbadet#mullerschupp,powersets,smartsucc,uselangext,uselangint,directsim",
"nbadet#mullerschupp,powersets,smartsucc,uselangext,uselangint,directsim,ascc,ascccyc,rscc,optdet,optmix",
"nbadet#safra",
"nbadet#safra,powersets",
"nbadet#safra,powersets,smartsucc",
"nbadet#safra,powersets,smartsucc,uselangext,uselangint,directsim",
"nbadet#safra,powersets,smartsucc,uselangext,uselangint,directsim,ascc,ascccyc,rscc,optdet,optmix",
"nbadet#maxmerge",
"nbadet#maxmerge,powersets",
"nbadet#maxmerge,powersets,smartsucc",
"nbadet#maxmerge,powersets,smartsucc,uselangext,uselangint,directsim",
"nbadet#maxmerge,powersets,smartsucc,uselangext,uselangint,directsim,ascc,ascccyc,rscc,optdet,optmix"
],
"data": "S"
},
"ltl2da": "ltl2da",
"ltl2na": "ltl2na",
"buchi-degen": {
......
......@@ -67,6 +67,40 @@
"simplify-ltl"
]
},
"nbadet": {
"type": "owl",
"input": "ltl",
"output": "hoa",
"name": "nbadet",
"flags": {
"default": "--default-config",
"mullerschupp": "-m0",
"safra": "-m1",
"maxmerge": "-m2",
"powersets": "-t",
"smartsucc": "-s",
"directsim": "-lrefinement",
"uselangext": "-e",
"uselangint": "-j",
"ascc": "-A",
"ascccyc": "-b",
"rscc": "-r",
"optdet": "-d",
"optmix": "-c"
},
"pre": [
"simplify-ltl",
[
"ltl2aut-ext",
"-t",
"'ltl2tgba -B -H'"
],
"optimize-aut"
],
"post": [
"optimize-aut"
]
},
"ltl2dra": {
"type": "owl",
"input": "ltl",
......@@ -289,6 +323,25 @@
"simplify-ltl",
"ltl2ngba"
]
},
"nbasim": {
"type": "owl",
"input": "ltl",
"output": "hoa",
"name": "nbasim",
"flags": {
"refinement": "--direct-refinement",
"direct": "--direct",
"delayed": "--delayed"
},
"pre": [
"simplify-ltl",
[
"ltl2aut-ext",
"-t",
"'ltl2tgba -B -H'"
]
]
}
},
"aliases": {
......
......@@ -21,6 +21,7 @@ package owl.automaton;
import com.google.auto.value.AutoValue;
import com.google.common.collect.Sets;
import java.util.BitSet;
import java.util.HashMap;
import java.util.HashSet;
......@@ -30,6 +31,7 @@ import java.util.Optional;
import java.util.Set;
import java.util.function.BiConsumer;
import java.util.function.IntConsumer;
import owl.automaton.Automaton.EdgeMapVisitor;
import owl.automaton.acceptance.GeneralizedBuchiAcceptance;
import owl.automaton.algorithm.LanguageEmptiness;
......@@ -201,4 +203,5 @@ public final class AutomatonUtil {
automaton, Set.copyOf(initialComponent));
}
}
}
......@@ -292,7 +292,7 @@ public final class BooleanOperations {
Pair<ValuationSetFactory, Boolean> factory) {
super(factory.fst(),
Pair.of(automaton1.initialStates(), automaton2.initialStates()),
Pair.allPairs(automaton1.initialStates(), automaton2.initialStates()),
intersectionAcceptance(List.of(automaton1.acceptance(), automaton2.acceptance())));
this.automaton1 = automaton1;
......
/*
* Copyright (C) 2016 - 2020 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package owl.automaton.algorithm.simulations;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;
import owl.automaton.Automaton;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.acceptance.ParityAcceptance;
import owl.automaton.algorithm.simulations.SimulationStates.MultipebbleSimulationState;
import owl.automaton.edge.Edge;
import owl.collections.Pair;
import owl.collections.ValuationSet;
import owl.factories.ValuationSetFactory;
import owl.run.Environment;
import owl.util.BitSetUtil;
public class BackwardDirectSimulation<S>
implements SimulationType<S, MultipebbleSimulationState<S>> {
Automaton<S, BuchiAcceptance> leftAutomaton;
Automaton<S, BuchiAcceptance> rightAutomaton;
ValuationSetFactory factory;
S leftState;
S rightState;
MultipebbleSimulationState<S> initialState;
MultipebbleSimulationState<S> sinkState;
int pebbleCount;
Set<Pair<S, S>> knownPairs;
public BackwardDirectSimulation(
Automaton<S, BuchiAcceptance> leftAutomaton,
Automaton<S, BuchiAcceptance> rightAutomaton,
S left,
S right,
int pebbleCount,
Set<Pair<S, S>> known
) {
this.leftAutomaton = leftAutomaton;
this.rightAutomaton = rightAutomaton;
this.leftState = left;
this.rightState = right;
this.pebbleCount = pebbleCount;
this.knownPairs = known;
this.factory = Environment
.annotated()
.factorySupplier()
.getValuationSetFactory(List.of("a"));
this.initialState = MultipebbleSimulationState.of(
Pebble.of(left, false),
MultiPebble.of(right, false, pebbleCount)
);
this.sinkState = MultipebbleSimulationState.of(
Pebble.of(left, true),
MultiPebble.of(List.of(), pebbleCount)
);
}
public static <S> BackwardDirectSimulation<S> of(
Automaton<S, BuchiAcceptance> leftAutomaton,
Automaton<S, BuchiAcceptance> rightAutomaton,
S leftState,
S rightState,
int pebbleCount,
Set<Pair<S, S>> known
) {
return new BackwardDirectSimulation<>(
leftAutomaton, rightAutomaton, leftState, rightState, pebbleCount, known
);
}
@Override
public Map<Edge<MultipebbleSimulationState<S>>, ValuationSet> edgeMap(
MultipebbleSimulationState<S> state
) {
Map<Edge<MultipebbleSimulationState<S>>, ValuationSet> out = new HashMap<>();
if (state.equals(sinkState)) {
out.put(Edge.of(sinkState, 1), factory.universe());
return out;
}
if (state.owner().isOdd()) {
if (state.even().isSingleton()
&& knownPairs.contains(Pair.of(state.odd().state(), state.even().onlyState()))) {
out.put(Edge.of(state, 0), factory.universe());
return out;
}
// check if Duplicator has a pebble on an initial state
boolean containsInitial = state.even().pebbles()
.stream().anyMatch(p -> rightAutomaton.initialStates().contains(p.state()));
if ((!containsInitial && leftAutomaton.initialStates().contains(state.odd().state()))
|| (!state.even().flag() && state.odd().flag())) {
// Spoiler reached an initial state while Duplicator did not, go to sink
out.put(Edge.of(sinkState, 1), factory.universe());
return out;
}
// we obtain the entrySet to be able to exit prematurely if no predecessors are available
var predecessors = leftAutomaton.predecessors(state.odd().state());
if (predecessors.isEmpty()) {
out.put(Edge.of(state, 0), factory.universe());
return out;
}
predecessors.forEach(pred -> {
leftAutomaton.edgeMap(pred).forEach((e, vS) -> {
if (e.successor().equals(state.odd().state())) {
vS.forEach(val -> {
state.odd().predecessors(leftAutomaton, val).forEach(p -> {
var target = MultipebbleSimulationState.of(
p, state.even().setFlag(false), val
);
out.put(Edge.of(target, 0), factory.universe());
});
});
}
});
});
} else {
var possibilities = state.even()
.predecessors(leftAutomaton, BitSetUtil.fromInt(state.valuation()));
if (possibilities.isEmpty()) {
out.put(Edge.of(sinkState, 1), factory.universe());
return out;
}
possibilities.forEach(p -> {
if (!state.odd().flag() || p.flag()) {
var target = MultipebbleSimulationState.of(
state.odd(), p
);
out.put(Edge.of(target, 0), factory.universe());
} else {
out.put(Edge.of(sinkState, 1), factory.universe());
}
});
}
return out;
}
@Override
public Set<MultipebbleSimulationState<S>> states() {
return MultipebbleSimulationState.universe(
Pebble.universe(leftAutomaton),
MultiPebble.universe(rightAutomaton, pebbleCount),
leftAutomaton.factory().universe()
);
}
@Override
public ParityAcceptance acceptance() {
return new ParityAcceptance(2, ParityAcceptance.Parity.MAX_EVEN);
}
@Override
public Set<MultipebbleSimulationState<S>> initialStates() {
return Set.of(initialState);
}
@Override
public ValuationSetFactory factory() {
return factory;
}
}
/*
* Copyright (C) 2016 - 2020 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package owl.automaton.algorithm.simulations;
import com.google.auto.value.AutoValue;
import org.apache.commons.cli.CommandLine;
import org.apache.commons.cli.Option;
import org.apache.commons.cli.Options;
@AutoValue
public abstract class BuchiSimulationArguments {
private static final Option optDirect = Option
.builder("di")
.longOpt("direct")
.desc("Compute direct simulation relation")
.build();
private static final Option optDirectRefinement = Option
.builder("diref")
.longOpt("direct-refinement")
.desc("Compute direct simulation relation using color refinement (fast)")
.build();
private static final Option optDelayed = Option
.builder("de")
.longOpt("delayed")
.desc("Compute delayed simulation relation")
.build();
private static final Option optFair = Option
.builder("f")
.longOpt("fair")
.desc("Compute fair simulation relation")
.build();
private static final Option optBackward = Option
.builder("bw")
.longOpt("backward")
.desc("Compute backwards simulation relation")
.build();
private static final Option optLookaheadDirect = Option
.builder("diL")
.longOpt("lookahead-direct")
.desc("Compute direct simulation with lookahead")
.build();
private static final Option optMaxLookahead = Option
.builder("l")
.longOpt("lookahead")
.desc("Make this many moves of Spoiler available to Duplicator")
.hasArg()
.argName("lookahead")
.type(Integer.class)
.build();
private static final Option optSanity = Option
.builder("S")
.longOpt("sanity")
.desc("Sanity check different relation inclusions for input automaton.")
.build();
private static final Option optPebbleCount = Option
.builder("c")
.longOpt("pebbles")
.desc("Allow duplicator to have the set amount of pebbles")
.hasArg()
.argName("pebbles")
.type(Integer.class)
.build();
private static final Option optVerboseFine = Option
.builder("V")
.longOpt("verbose")
.desc("Use logging level FINE for more output")
.build();
public static Options options = new Options()
.addOption(optDirect)
.addOption(optVerboseFine)
.addOption(optDelayed)
.addOption(optBackward)
.addOption(optDirectRefinement)
.addOption(optMaxLookahead)
.addOption(optLookaheadDirect)
.addOption(optSanity)
.addOption(optFair)
.addOption(optPebbleCount);
public static Builder builder() {
return new AutoValue_BuchiSimulationArguments.Builder()
.setPebbleCount(1)
.setVerboseFine(false)
.setComputeFair(false)
.setComputeLookaheadDirect(false)
.setMaxLookahead(1)
.setSanity(false)
.setComputeBackward(false)
.setComputeDelayed(false)
.setComputeDirect(true)
.setComputeDirectRefinement(false);
}
public static BuchiSimulationArguments getFromCli(CommandLine cmdLine) {
var builder = builder();
builder.setComputeDirect(cmdLine.hasOption(optDirect.getOpt()));
if (cmdLine.hasOption(optDelayed.getOpt())) {
builder.setComputeDelayed(true);
// since direct is contained in delayed, we can switch this off
builder.setComputeDirect(false);
}
if (cmdLine.hasOption(optFair.getOpt())) {
builder.setComputeFair(true);
// since both are contained in fair simulation we switch them off
builder.setComputeDelayed(false);
builder.setComputeDirect(false);
}
if (cmdLine.hasOption(optBackward.getOpt())) {
builder.setComputeBackward(true);
builder.setComputeDirect(false);
builder.setComputeDelayed(false);
builder.setComputeFair(false);
}
if (cmdLine.hasOption(optLookaheadDirect.getOpt())) {
builder.setComputeBackward(false);
builder.setComputeDirect(false);
builder.setComputeDelayed(false);
builder.setComputeFair(false);
builder.setComputeLookaheadDirect(true);
}
if (cmdLine.hasOption(optDirectRefinement.getOpt())) {
builder.setComputeBackward(false);
builder.setComputeDirect(false);
builder.setComputeDelayed(false);
builder.setComputeFair(false);
builder.setComputeLookaheadDirect(false);
builder.setComputeDirectRefinement(true);
}
builder.setSanity(cmdLine.hasOption(optSanity.getOpt()));
builder.setVerboseFine(cmdLine.hasOption(optVerboseFine.getOpt()));
if (cmdLine.hasOption(optPebbleCount.getOpt())) {
builder.setPebbleCount(Integer.parseInt(cmdLine.getOptionValue(optPebbleCount.getOpt())));
}
if (cmdLine.hasOption(optMaxLookahead.getOpt())) {
builder.setMaxLookahead(Integer.parseInt(cmdLine.getOptionValue(optMaxLookahead.getOpt())));
}
return builder.build();
}
public abstract boolean computeDirect();
public abstract boolean computeDelayed();
public abstract boolean computeFair();
public abstract boolean computeBackward();
public abstract boolean computeLookaheadDirect();
public abstract boolean computeDirectRefinement();
public abstract boolean sanity();
public abstract int pebbleCount();
public abstract int maxLookahead();
public abstract boolean verboseFine();
@AutoValue.Builder
abstract static class Builder {
abstract Builder setComputeDirect(boolean b);
abstract Builder setComputeDelayed(boolean b);
abstract Builder setComputeFair(boolean b);
abstract Builder setComputeBackward(boolean b);
abstract Builder setComputeLookaheadDirect(boolean b);
abstract Builder setComputeDirectRefinement(boolean b);
abstract Builder setSanity(boolean b);
abstract Builder setPebbleCount(int count);
abstract Builder setMaxLookahead(int lookahead);
abstract Builder setVerboseFine(boolean b);