Commit 7c4ffe37 authored by Tobias MEGGENDORFER's avatar Tobias MEGGENDORFER
Browse files

Changes

parent c7c08603
......@@ -37,7 +37,7 @@ dependencies {
// Owl
implementation(files("lib/owl-21.0.jar", "lib/jhoafparser-1.1.1-patched.jar"))
implementation("de.tum.in", "jbdd", "0.5.2")
implementation("de.tum.in", "naturals-util", "0.16.0")
implementation("de.tum.in", "naturals-util", "0.17.0")
implementation("commons-cli", "commons-cli", "1.4")
implementation("org.antlr", "antlr4-runtime", "4.8-1")
......
package com.cges.algorithm;
import static owl.automaton.acceptance.ParityAcceptance.Parity;
import com.cges.graph.HistoryGame;
import com.cges.graph.HistoryGame.HistoryState;
import com.cges.graph.SuspectGame;
......@@ -8,27 +10,22 @@ import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.Move;
import com.cges.model.PayoffAssignment;
import com.cges.model.Transition;
import com.cges.parity.OinkGameSolver;
import com.cges.parity.Player;
import com.cges.parity.PriorityState;
import com.cges.parity.Solution;
import com.cges.parity.SuspectParityGame;
import java.util.ArrayDeque;
import java.util.EnumSet;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import javax.annotation.Nullable;
import owl.automaton.Automaton;
import owl.automaton.ParityUtil;
import owl.automaton.acceptance.ParityAcceptance;
import owl.ltl.BooleanConstant;
import owl.ltl.Conjunction;
import owl.ltl.Disjunction;
import owl.ltl.GOperator;
......@@ -44,30 +41,17 @@ public final class DeviationSolver<S> implements PunishmentStrategy<S> {
private static final Function<LabelledFormula, Automaton<?, ? extends ParityAcceptance>> translation =
LtlTranslationRepository.LtlToDpaTranslation.SEJK16_EKRS17.translation(EnumSet.of(Option.SIMPLIFY_AUTOMATON));
private static final Function<LabelledFormula, Automaton<?, ? extends ParityAcceptance>> referenceTranslation =
LtlTranslationRepository.defaultTranslation(EnumSet.of(Option.COMPLETE),
LtlTranslationRepository.BranchingMode.DETERMINISTIC, ParityAcceptance.class);
@SuppressWarnings("unchecked")
private static final Function<LabelledFormula, Automaton<Object, ParityAcceptance>> referenceFunction =
formula -> (Automaton<Object, ParityAcceptance>) referenceTranslation.apply(formula);
private final SuspectGame<S> suspectGame;
private final Map<LabelledFormula, Automaton<?, ?>> automatonCache = new HashMap<>();
private final OinkGameSolver solver = new OinkGameSolver();
private final Map<Agent, Literal> agentLiterals;
private final List<String> atomicPropositions;
private final Set<Agent> losingAgents;
private final Map<HistoryState<S>, Map<Move, PriorityState<S>>> initialStates;
private final Map<PriorityState<S>, PriorityState<S>> strategy;
@Nullable
private final SuspectParityGame<S> game;
@SuppressWarnings("unchecked")
private final Function<LabelledFormula, Automaton<Object, ParityAcceptance>> dpaCachingFunction = formula ->
(Automaton<Object, ParityAcceptance>) automatonCache.computeIfAbsent(formula,
f -> ParityUtil.convert(translation.apply(f), ParityAcceptance.Parity.MIN_EVEN));
private final SuspectParityGame<S> parityGame;
private final Solution<PriorityState<S>> paritySolution;
public DeviationSolver(SuspectGame<S> suspectGame, PayoffAssignment payoff) {
this.suspectGame = suspectGame;
......@@ -80,61 +64,14 @@ public final class DeviationSolver<S> implements PunishmentStrategy<S> {
a -> Literal.of(atomicPropositions.indexOf(a.name()))));
assert Set.copyOf(atomicPropositions).size() == atomicPropositions.size();
// TODO Properly do the cache -- it should be possible to solve the complete history game through the initial state only
var historyState = historyGame.initialState();
var eveState = new EveState<S>(historyState, losingAgents);
var goal = SimplifierRepository.SYNTACTIC_FAIRNESS.apply(LabelledFormula.of(Disjunction.of(losingAgents.stream()
.map(a -> Conjunction.of(GOperator.of(agentLiterals.get(a)), historyState.goal(a)))).not(), atomicPropositions));
EveState<S> eveState = new EveState<>(historyState, losingAgents);
LabelledFormula eveGoal = LabelledFormula.of(Disjunction.of(losingAgents.stream()
.map(a -> Conjunction.of(GOperator.of(agentLiterals.get(a)), historyState.goal(a)))).not(), atomicPropositions);
var goal = SimplifierRepository.SYNTACTIC_FAIRNESS.apply(eveGoal);
if (goal.formula() instanceof BooleanConstant) {
strategy = Map.of();
initialStates = Map.of();
game = null;
} else {
var gameSolution = solveParityGame(eveState, goal);
game = gameSolution.parityGame();
var paritySolution = gameSolution.solution();
Set<PriorityState<S>> solvedTopLevelEveStates = game.states().stream()
.filter(p -> p.isEve() && p.eve().suspects().equals(losingAgents))
.collect(Collectors.toSet());
Queue<PriorityState<S>> queue = new ArrayDeque<>();
solvedTopLevelEveStates.stream().filter(p -> paritySolution.winner(p) == Player.ODD).forEach(queue::add);
Set<PriorityState<S>> reached = new HashSet<>();
Map<PriorityState<S>, PriorityState<S>> strategy = new HashMap<>();
while (!queue.isEmpty()) {
PriorityState<S> next = queue.poll();
assert paritySolution.winner(next) == Player.ODD;
Stream<PriorityState<S>> successors;
if (game.owner(next) == Player.EVEN) {
successors = game.successors(next);
} else {
PriorityState<S> successor = paritySolution.oddStrategy().get(next);
strategy.put(next, successor);
successors = Stream.of(successor);
}
successors.forEach(successor -> {
if (reached.add(successor)) {
queue.add(successor);
}
});
}
this.strategy = Map.copyOf(strategy);
Map<HistoryState<S>, Map<Move, PriorityState<S>>> initialStates = new HashMap<>();
for (PriorityState<S> priorityState : solvedTopLevelEveStates) {
HistoryState<S> gameHistoryState = priorityState.eve().historyState();
Map<Move, PriorityState<S>> winningInitial = new HashMap<>();
game.successors(priorityState)
.filter(s -> paritySolution.winner(s) == Player.ODD)
.forEach(winner -> winningInitial.put(winner.adam().move(), winner));
initialStates.put(gameHistoryState, Map.copyOf(winningInitial));
}
this.initialStates = Map.copyOf(initialStates);
}
var gameSolution = solveParityGame(eveState, goal);
parityGame = gameSolution.parityGame();
paritySolution = gameSolution.solution();
}
private LabelledFormula eveGoal(HistoryState<S> historyState) {
......@@ -142,48 +79,48 @@ public final class DeviationSolver<S> implements PunishmentStrategy<S> {
.map(a -> Conjunction.of(GOperator.of(agentLiterals.get(a)), historyState.goal(a)))).not(), atomicPropositions);
}
public boolean isWinning(HistoryState<S> historyState, Move move) {
Map<Move, PriorityState<S>> winningMoves = this.initialStates.get(historyState);
if (winningMoves == null) {
LabelledFormula eveGoal = eveGoal(historyState);
var goal = SimplifierRepository.SYNTACTIC_FAIRNESS.apply(eveGoal).formula();
assert goal instanceof BooleanConstant;
assert computeWinning(historyState) == ((BooleanConstant) goal).value;
return ((BooleanConstant) goal).value;
}
return winningMoves.containsKey(move);
public Stream<Move> winningMoves(HistoryState<S> historyState) {
return suspectGame.historyGame().transitions(historyState)
.map(Transition::move)
.filter(m -> isWinning(historyState, m));
}
public boolean isWinning(HistoryState<S> historyState, Move proposedMove) {
return parityGame.deviationStates(historyState, proposedMove).map(paritySolution::winner).allMatch(Player.ODD::equals);
}
private boolean computeWinning(HistoryState<S> historyState) {
var solution = solveParityGame(new EveState<>(historyState, losingAgents), eveGoal(historyState));
return solution.solution().winner(solution.parityGame().initialState()) == Player.ODD;
return suspectGame.historyGame().transitions(historyState).map(Transition::move)
.anyMatch(move -> solution.parityGame.deviationStates(historyState, move)
.map(solution.solution()::winner)
.allMatch(Player.ODD::equals));
}
@Override
public Set<PriorityState<S>> initialStates(HistoryState<S> state, Move proposedMove) {
PriorityState<S> initialAdam = initialStates.get(state).get(proposedMove);
return game == null ? Set.of(initialAdam) : game.successors(initialAdam).collect(Collectors.toSet());
public Set<PriorityState<S>> states(HistoryState<S> state, Move proposedMove) {
return parityGame.deviationStates(state, proposedMove).collect(Collectors.toSet());
}
@Override
public PriorityState<S> move(PriorityState<S> state) {
assert state.isEve();
return strategy.getOrDefault(state, state);
PriorityState<S> successor = paritySolution.oddStrategy().get(state);
assert !successor.isEve() : "Non-alternating players in %s -> %s".formatted(state, successor);
return successor;
}
@Override
public Set<PriorityState<S>> successors(PriorityState<S> state) {
if (state.isEve()) {
return Set.of(move(state));
}
return game == null ? Set.of(state) : game.successors(state).collect(Collectors.toSet());
return state.isEve() ? Set.of(move(state)) : parityGame.successors(state).collect(Collectors.toSet());
}
record ParitySolution<S>(SuspectParityGame<S> parityGame, Solution<PriorityState<S>> solution) {}
private ParitySolution<S> solveParityGame(EveState<S> eveState, LabelledFormula goal) {
var shifted = LiteralMapper.shiftLiterals(goal);
var automaton = dpaCachingFunction.apply(shifted.formula);
@SuppressWarnings("unchecked")
var automaton = (Automaton<Object, ParityAcceptance>) ParityUtil.convert(translation.apply(shifted.formula), Parity.MIN_EVEN);
assert !automaton.states().isEmpty();
var parityGame = SuspectParityGame.create(suspectGame, eveState, automaton);
var paritySolution = solver.solve(parityGame);
......
......@@ -6,7 +6,7 @@ import com.cges.parity.PriorityState;
import java.util.Set;
public interface PunishmentStrategy<S> {
Set<PriorityState<S>> initialStates(HistoryGame.HistoryState<S> state, Move proposedMove);
Set<PriorityState<S>> states(HistoryGame.HistoryState<S> state, Move proposedMove);
PriorityState<S> move(PriorityState<S> state);
......
......@@ -5,6 +5,7 @@ import com.cges.model.ConcurrentGame;
import com.cges.model.Transition;
import com.google.common.collect.Lists;
import de.tum.in.naturals.Indices;
import it.unimi.dsi.fastutil.objects.Object2IntMap;
import java.util.ArrayDeque;
import java.util.Arrays;
import java.util.BitSet;
......@@ -22,8 +23,7 @@ import owl.ltl.Formula;
import owl.ltl.rewriter.SimplifierRepository;
public class FormulaHistoryGame<S> implements HistoryGame<S> {
private final Map<Agent, Integer> indices;
private final Object2IntMap<Agent> indices;
static final class ListHistoryState<S> implements HistoryState<S> {
private static final Formula[] EMPTY = new Formula[0];
......@@ -42,7 +42,7 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
@Override
public Formula goal(Agent agent) {
return agentGoals[game.indices.get(agent)];
return agentGoals[game.indices.getInt(agent)];
}
@Override
......@@ -75,7 +75,7 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
@Override
public String toString() {
return state + " " + game.indices.entrySet().stream().sorted(Map.Entry.comparingByKey(Comparator.comparing(Agent::name)))
return state + " " + game.indices.object2IntEntrySet().stream().sorted(Map.Entry.comparingByKey(Comparator.comparing(Agent::name)))
.map(Map.Entry::getValue)
.map(i -> agentGoals[i])
.map(SimplifierRepository.SYNTACTIC_FIXPOINT::apply)
......@@ -91,11 +91,8 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
public FormulaHistoryGame(ConcurrentGame<S> game) {
this.game = game;
Map<String, Integer> propositionIndices = new HashMap<>();
Indices.forEachIndexed(game.atomicPropositions(), (index, proposition) -> propositionIndices.put(proposition, index));
Map<Agent, Integer> agentIndices = new HashMap<>();
Indices.forEachIndexed(game.agents(), (index, agent) -> agentIndices.put(agent, index));
indices = Map.copyOf(agentIndices);
var propositionIndices = Indices.ids(game.atomicPropositions());
indices = Indices.ids(game.agents());
this.initialState = new ListHistoryState<>(game.initialState(),
game.agents().stream().map(Agent::goal).map(Formula::unfold).toList(), this);
......@@ -109,7 +106,7 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
BitSet valuation = labelCache.computeIfAbsent(state.state(), s -> {
BitSet set = new BitSet();
game.labels(s).stream().map(propositionIndices::get).forEach(set::set);
game.labels(s).stream().map(propositionIndices::getInt).forEach(set::set);
return set;
});
List<Formula> successorGoals = List.copyOf(Lists.transform(state.goals(), goal -> goal.temporalStep(valuation).unfold()));
......
......@@ -6,7 +6,6 @@ import com.cges.graph.HistoryGame.HistoryState;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.PayoffAssignment;
import com.cges.model.Transition;
import com.cges.output.DotFormatted;
import java.util.BitSet;
import java.util.Comparator;
......@@ -68,7 +67,7 @@ public final class RunGraph<S> {
public Set<RunState<S>> initialStates() {
HistoryState<S> initialState = historyGame.initialState();
if (historyGame.transitions(initialState).map(Transition::move).anyMatch(m -> deviationSolver.isWinning(initialState, m))) {
if (deviationSolver.winningMoves(initialState).findAny().isPresent()) {
return automaton.initialStates().stream()
.map(s -> new RunState<>(s, initialState))
.collect(Collectors.toSet());
......@@ -96,8 +95,9 @@ public final class RunGraph<S> {
if (automatonEdges.isEmpty()) {
return Set.of();
}
var transitions = historyGame.transitions(current.historyState())
.filter(t -> deviationSolver.isWinning(current.historyState(), t.move()))
HistoryState<S> historyState = current.historyState();
var transitions = historyGame.transitions(historyState)
.filter(t -> deviationSolver.isWinning(historyState, t.move()))
.flatMap(transition -> automatonEdges.stream().map(edge ->
new RunTransition<>(new RunState<>(edge.successor(), transition.destination()), !edge.colours().isEmpty())))
.collect(Collectors.toSet());
......
......@@ -40,7 +40,7 @@ public final class SuspectGame<S> {
}
public Stream<AdamState<S>> successors(EveState<S> eveState) {
return Set.copyOf(transitions.computeIfAbsent(eveState, this::computeDeviatingSuccessors).keySet()).stream();
return game.transitions(eveState.historyState()).map(Transition::move).map(move -> new AdamState<>(eveState, move));
}
public Stream<EveState<S>> successors(AdamState<S> adamState) {
......@@ -58,7 +58,7 @@ public final class SuspectGame<S> {
public Stream<EveState<S>> eveSuccessors(EveState<S> eveState) {
return Stream.concat(transitions.computeIfAbsent(eveState, this::computeDeviatingSuccessors)
.values().stream().flatMap(Collection::stream),
.values().stream().flatMap(Collection::stream),
game.transitions(eveState.historyState()).map(t -> new EveState<S>(t.destination(), eveState.suspects())));
}
......
......@@ -271,7 +271,7 @@ public final class DotWriter {
writer.append("digraph {\n");
Set<RunGraph.RunState<S>> loopStates = lasso.states(false).collect(Collectors.toSet());
Set<PriorityState<S>> reachableGameStates = loopStates.stream()
.flatMap(runState -> punishmentStrategy.initialStates(runState.historyState(), moves.get(runState))
.flatMap(runState -> punishmentStrategy.states(runState.historyState(), moves.get(runState))
.stream().filter(s -> !s.eve().historyState().equals(lasso.successor(runState).historyState())))
.collect(Collectors.toSet());
Queue<PriorityState<S>> queue = new ArrayDeque<>(reachableGameStates);
......@@ -320,9 +320,9 @@ public final class DotWriter {
loopIds.forEach((runState, id) -> {
Move move = strategy.moves().get(runState);
writer.append("HS_%d -> HS_%d [label=\"%s\",penwidth=2];\n".formatted(id, loopIds.getInt(lasso.successor(runState)),
toDotString(move)));
punishmentStrategy.initialStates(runState.historyState(), move)
writer.append("HS_%d -> HS_%d [label=\"%s\",penwidth=2];\n"
.formatted(id, loopIds.getInt(lasso.successor(runState)), toDotString(move)));
punishmentStrategy.states(runState.historyState(), move)
.stream().filter(s -> !s.eve().historyState().equals(lasso.successor(runState).historyState()))
.forEach(punishmentState -> writer.append("HS_%d -> GS_%d [style=dotted];\n".formatted(id, gameIds.getInt(punishmentState))));
});
......
......@@ -5,6 +5,8 @@ import static java.util.Objects.requireNonNull;
import com.google.common.util.concurrent.ThreadFactoryBuilder;
import com.google.common.util.concurrent.Uninterruptibles;
import de.tum.in.naturals.map.Nat2ObjectDenseArrayMap;
import it.unimi.dsi.fastutil.ints.Int2ObjectMap;
import it.unimi.dsi.fastutil.ints.IntOpenHashSet;
import it.unimi.dsi.fastutil.ints.IntSet;
import it.unimi.dsi.fastutil.objects.Object2IntMap;
......@@ -14,16 +16,13 @@ import java.io.BufferedWriter;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.OutputStreamWriter;
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.ExecutorService;
......@@ -64,39 +63,22 @@ public final class OinkGameSolver {
public <S> Solution<S> solve(ParityGame<S> game) {
Object2IntMap<S> oinkNumbering = new Object2IntOpenHashMap<>();
oinkNumbering.defaultReturnValue(-1);
oinkNumbering.put(game.initialState(), 0);
List<S> reverseMapping = new ArrayList<>();
reverseMapping.add(game.initialState());
Queue<Indexed<S>> queue = new ArrayDeque<>(List.of(new Indexed<>(game.initialState(), 0)));
IntSet[] successorIdsBuild = new IntSet[128];
while (!queue.isEmpty()) {
Indexed<S> state = queue.poll();
assert state.index() == oinkNumbering.getInt(state.object());
game.forEachState(s -> {
int id = oinkNumbering.size();
oinkNumbering.put(s, id);
reverseMapping.add(s);
});
Int2ObjectMap<IntSet> successorIds = new Nat2ObjectDenseArrayMap<>(128);
oinkNumbering.forEach((state, id) -> {
IntSet stateSuccessorIds = new IntOpenHashSet();
game.successors(state.object()).distinct().forEach(successor -> {
int newId = oinkNumbering.size();
int existingId = oinkNumbering.putIfAbsent(successor, newId);
if (existingId == -1) {
reverseMapping.add(successor);
queue.add(new Indexed<>(successor, newId));
stateSuccessorIds.add(newId);
} else {
stateSuccessorIds.add(existingId);
}
});
if (successorIdsBuild.length <= state.index()) {
successorIdsBuild = Arrays.copyOf(successorIdsBuild, Math.max(state.index() + 1, successorIdsBuild.length * 2));
}
successorIdsBuild[state.index()] = stateSuccessorIds;
}
assert oinkNumbering.object2IntEntrySet().stream().allMatch(entry -> entry.getKey().equals(reverseMapping.get(entry.getIntValue())));
game.successors(state).mapToInt(oinkNumbering::getInt).forEach(stateSuccessorIds::add);
successorIds.put(id.intValue(), stateSuccessorIds);
});
IntSet[] successorIds = successorIdsBuild;
assert oinkNumbering.object2IntEntrySet().stream().allMatch(entry -> entry.getKey().equals(reverseMapping.get(entry.getIntValue())));
assert IntStream.range(0, oinkNumbering.size()).allMatch(i ->
game.successors(reverseMapping.get(i)).map(oinkNumbering::getInt).collect(Collectors.toSet()).equals(successorIds[i]));
game.successors(reverseMapping.get(i)).map(oinkNumbering::getInt).collect(Collectors.toSet()).equals(successorIds.get(i)));
ProcessBuilder oinkProcessBuilder = new ProcessBuilder(OINK_EXECUTION);
oinkProcessBuilder.redirectErrorStream(true);
......@@ -154,7 +136,7 @@ public final class OinkGameSolver {
writer.append(String.valueOf(index)).append(' ')
.append(String.valueOf(game.priority(state))).append(' ')
.append(String.valueOf(game.owner(state).id()));
var successorIterator = successorIds[index].intIterator();
var successorIterator = successorIds.get(index).intIterator();
if (successorIterator.hasNext()) {
writer.append(' ').append(String.valueOf(successorIterator.nextInt()));
while (successorIterator.hasNext()) {
......
package com.cges.parity;
import java.util.ArrayDeque;
import java.util.HashSet;
import java.util.List;
import java.util.Queue;
import java.util.Set;
import java.util.function.Consumer;
import java.util.stream.Stream;
public interface ParityGame<S> {
S initialState();
default Set<S> states() {
Set<S> reached = new HashSet<>(List.of(initialState()));
Queue<S> queue = new ArrayDeque<>(reached);
while (!queue.isEmpty()) {
successors(queue.poll()).forEach(successor -> {
if (reached.add(successor)) {
queue.add(successor);
}
});
}
return reached;
}
Set<S> states();
Stream<S> successors(S state);
int priority(S state);
default void forEachState(Consumer<S> action) {
Set<S> reached = new HashSet<>(List.of(initialState()));
Queue<S> queue = new ArrayDeque<>(reached);
while (!queue.isEmpty()) {
S state = queue.poll();
successors(state).forEach(successor -> {
if (reached.add(successor)) {
action.accept(successor);
queue.add(successor);
}
});
}
states().forEach(action);
}
Player owner(S state);
......
......@@ -2,36 +2,43 @@ package com.cges.parity;
import static com.google.common.base.Preconditions.checkArgument;
import com.cges.graph.HistoryGame;
import com.cges.graph.SuspectGame;
import com.cges.graph.SuspectGame.EveState;
import com.cges.model.Agent;
import com.cges.model.Move;
import com.cges.model.Transition;
import com.google.common.collect.ImmutableSetMultimap;
import com.google.common.collect.ImmutableTable;
import com.google.common.collect.SetMultimap;
import com.google.common.collect.Table;
import de.tum.in.naturals.Indices;
import de.tum.in.naturals.bitset.BitSets;
import it.unimi.dsi.fastutil.objects.Object2IntMap;
import java.util.ArrayDeque;
import java.util.BitSet;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.Queue;
import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;
import java.util.stream.IntStream;
import java.util.stream.Stream;
import owl.automaton.Automaton;
import owl.automaton.acceptance.ParityAcceptance;
import owl.automaton.edge.Edge;
public final class SuspectParityGame<S> implements ParityGame<PriorityState<S>> {
private final SuspectGame<S> suspectGame;
private final PriorityState<S> initialState;
private final Automaton<Object, ParityAcceptance> dpa;
private final Map<S, BitSet> gameStateLabelCache;
private final int maximumPriority;
private final Map<String, Integer> propositionIndex;
private SuspectParityGame(SuspectGame<S> suspectGame, PriorityState<S> initialState, Automaton<Object, ParityAcceptance> dpa) {
private final SetMultimap<HistoryGame.HistoryState<S>, NonDeviationState<S>> historyStateMap;
private final Table<NonDeviationState<S>, Move, Set<PriorityState<S>>> deviationSuccessors;
private final SetMultimap<PriorityState<S>, PriorityState<S>> successors;
private SuspectParityGame(SuspectGame<S> suspectGame, EveState<S> initialState, Automaton<Object, ParityAcceptance> dpa) {
assert !dpa.acceptance().parity().max();
this.suspectGame = suspectGame;
this.initialState = initialState;
this.dpa = dpa;
// We have a min even objective and want max + let eve be odd player
int maximumPriority = dpa.acceptance().acceptanceSets();
......@@ -39,48 +46,109 @@ public final class SuspectParityGame<S> implements ParityGame<PriorityState<S>>
// Ensure that maximum priority is odd, so if priority is even then maximum priority is odd
maximumPriority += 1;
}
this.maximumPriority = maximumPriority;
List<String> propositions = dpa.atomicPropositions();
propositionIndex = IntStream.range(0, propositions.size())
.boxed()
.collect(Collectors.toMap(propositions::get, Function.identity()));
gameStateLabelCache = new HashMap<>();
Object2IntMap<String> propositionIndex = Indices.ids(propositions);
propositionIndex.defaultReturnValue(-1);
Map<S, BitSet> gameStateLabelCache = new HashMap<>();
Function<S, BitSet> gameStateLabels = s -> BitSets.copyOf(gameStateLabelCache.computeIfAbsent(s, state -> {
BitSet set = new BitSet();
suspectGame.historyGame().concurrentGame().labels(state).stream()
.mapToInt(propositionIndex::getInt)
.filter(i -> i >= 0)
.forEach(set::set);
return set;
}));
Set<Agent> initialSuspects = initialState.suspects();
BitSet allSuspectsLabel = new BitSet();
initialSuspects.stream().map(Agent::name).mapToInt(propositionIndex::getInt).filter(i -> i >= 0).forEach(allSuspectsLabel::set);
HistoryGame<S> historyGame = suspectGame.historyGame();