Commit d9fbf4f4 authored by Tobias MEGGENDORFER's avatar Tobias MEGGENDORFER
Browse files

.

parent 95d5bdc6
......@@ -12,6 +12,7 @@ import com.cges.model.PayoffAssignment;
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;
......@@ -59,7 +60,9 @@ public final class DeviationSolver<S> {
private final Map<Agent, Literal> agentLiterals;
private final List<String> atomicPropositions;
private final Set<Agent> losingAgents;
private final Map<HistoryState<S>, PunishmentStrategy<S>> cache = new HashMap<>();
private final Map<HistoryState<S>, Boolean> isWinning;
private final Map<HistoryState<S>, PriorityState<S>> initialStates;
private final Map<PriorityState<S>, PriorityState<S>> strategy;
@SuppressWarnings("unchecked")
private final Function<LabelledFormula, Automaton<Object, ParityAcceptance>> dpaCachingFunction = formula ->
......@@ -78,90 +81,109 @@ public final class DeviationSolver<S> {
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
doSolve(historyGame.initialState());
}
public Optional<PunishmentStrategy<S>> solve(HistoryState<S> historyState) {
assert cache.containsKey(historyState) || (SimplifierRepository.SYNTACTIC_FAIRNESS.apply(Disjunction.of(losingAgents.stream()
.map(a -> Conjunction.of(GOperator.of(agentLiterals.get(a)), historyState.goal(a)))).not()) instanceof BooleanConstant);
if (cache.containsKey(historyState)) {
PunishmentStrategy<S> strategy = cache.get(historyState);
assert doSolve(historyState).isPresent() == (strategy != null);
return Optional.ofNullable(strategy);
}
return doSolve(historyState);
}
var historyState = historyGame.initialState();
private Optional<PunishmentStrategy<S>> doSolve(HistoryState<S> historyState) {
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);
EveState<S> eveState = new EveState<>(historyState, losingAgents);
var goal = SimplifierRepository.SYNTACTIC_FAIRNESS.apply(eveGoal);
if (goal.formula() instanceof BooleanConstant bool) {
if (bool.value) {
PriorityState<S> state = new PriorityState<>(null, eveState, 0);
Strategy<S> strategy = new Strategy<>(state, Map.of(state, state));
cache.put(historyState, strategy);
return Optional.of(strategy);
if (goal.formula() instanceof BooleanConstant) {
isWinning = Map.of();
strategy = Map.of();
initialStates = Map.of();
} else {
var gameSolution = solveParityGame(eveState, goal);
var parityGame = gameSolution.parityGame();
var paritySolution = gameSolution.solution();
Set<PriorityState<S>> solvedTopLevelEveStates = parityGame.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 (parityGame.owner(next) == Player.EVEN) {
successors = parityGame.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);
}
});
}
cache.put(historyState, null);
return Optional.empty();
}
var shifted = LiteralMapper.shiftLiterals(goal);
var automaton = dpaCachingFunction.apply(shifted.formula);
if (automaton.states().isEmpty()) {
cache.put(historyState, null);
return Optional.empty();
}
var parityGame = SuspectParityGame.create(suspectGame, eveState, automaton);
var paritySolution = solver.solve(parityGame);
this.strategy = Map.copyOf(strategy);
Map<HistoryState<S>, Boolean> isWinning = new HashMap<>();
Set<PriorityState<S>> solvedTopLevelEveStates = parityGame.states().stream()
.filter(p -> p.isEve() && p.eve().suspects().equals(losingAgents))
.collect(Collectors.toSet());
System.out.println(solvedTopLevelEveStates);
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 (parityGame.owner(next) == Player.EVEN) {
successors = parityGame.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);
Map<HistoryState<S>, PriorityState<S>> initialStates = new HashMap<>();
for (PriorityState<S> priorityState : solvedTopLevelEveStates) {
HistoryState<S> gameHistoryState = priorityState.eve().historyState();
boolean stateWinning = paritySolution.winner(priorityState) == Player.ODD;
isWinning.put(gameHistoryState, stateWinning);
if (stateWinning) {
initialStates.put(gameHistoryState, priorityState);
}
});
}
this.initialStates = Map.copyOf(initialStates);
this.isWinning = Map.copyOf(isWinning);
}
}
var strategyCopy = Map.copyOf(strategy);
for (PriorityState<S> priorityState : solvedTopLevelEveStates) {
HistoryState<S> gameHistoryState = priorityState.eve().historyState();
if (paritySolution.winner(priorityState) == Player.ODD) {
assert !cache.containsKey(gameHistoryState) || cache.get(gameHistoryState) != null;
cache.putIfAbsent(gameHistoryState, new Strategy<>(priorityState, strategyCopy));
} else {
assert !cache.containsKey(gameHistoryState) || cache.get(gameHistoryState) == null;
cache.putIfAbsent(gameHistoryState, null);
private LabelledFormula eveGoal(HistoryState<S> historyState) {
return LabelledFormula.of(Disjunction.of(losingAgents.stream()
.map(a -> Conjunction.of(GOperator.of(agentLiterals.get(a)), historyState.goal(a)))).not(), atomicPropositions);
}
private Optional<PunishmentStrategy<S>> doSolve(HistoryState<S> historyState) {
Boolean winning = this.isWinning.get(historyState);
if (winning == null) {
LabelledFormula eveGoal = eveGoal(historyState);
var goal = SimplifierRepository.SYNTACTIC_FAIRNESS.apply(eveGoal).formula();
assert goal instanceof BooleanConstant;
boolean value = ((BooleanConstant) goal).value;
if (value) {
PriorityState<S> state = new PriorityState<>(null, new EveState<>(historyState, losingAgents), 1);
return Optional.of(new Strategy<>(state, Map.of(state, state)));
}
} else {
if (winning) {
return Optional.of(new Strategy<>(initialStates.get(historyState), strategy));
}
}
if (paritySolution.winner(parityGame.initialState()) == Player.EVEN) {
return Optional.empty();
}
return Optional.of(new Strategy<>(parityGame.initialState(), strategyCopy));
return Optional.empty();
}
public Optional<PunishmentStrategy<S>> solve(HistoryState<S> historyState) {
var solution = doSolve(historyState);
assert computeWinning(historyState) == solution.isPresent();
return solution;
}
private boolean computeWinning(HistoryState<S> historyState) {
var solution = solveParityGame(new EveState<>(historyState, losingAgents), eveGoal(historyState));
return solution.solution().winner(solution.parityGame().initialState()) == Player.ODD;
}
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);
assert !automaton.states().isEmpty();
var parityGame = SuspectParityGame.create(suspectGame, eveState, automaton);
var paritySolution = solver.solve(parityGame);
return new ParitySolution<>(parityGame, paritySolution);
}
public interface PunishmentStrategy<S> {
......
package com.cges.algorithm;
import com.cges.graph.RunGraph;
import com.cges.graph.RunGraph.RunState;
import com.cges.model.AcceptingLasso;
import com.cges.model.EquilibriumStrategy;
import com.cges.model.Move;
import com.cges.model.Transition;
import java.util.ArrayDeque;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.Queue;
import java.util.Set;
import java.util.stream.Collectors;
public final class RunGraphSolver {
......@@ -18,12 +23,12 @@ public final class RunGraphSolver {
private static <S> boolean validate(EquilibriumStrategy<S> strategy, RunGraph<S> graph) {
var lasso = strategy.lasso();
assert graph.initialStates().contains(lasso.states(true).iterator().next());
List<RunGraph.RunState<S>> loopStates = lasso.loopStates(true).toList();
List<RunState<S>> loopStates = lasso.loopStates(true).toList();
assert loopStates.size() >= 2;
boolean isAccepting = false;
for (int i = 0; i < loopStates.size() - 1; i++) {
RunGraph.RunState<S> current = loopStates.get(i);
RunGraph.RunState<S> successor = loopStates.get(i + 1);
RunState<S> current = loopStates.get(i);
RunState<S> successor = loopStates.get(i + 1);
var historySuccessor = graph.suspectGame().historyGame()
.transition(current.historyState(), strategy.moves().get(current))
.map(Transition::destination)
......@@ -43,21 +48,32 @@ public final class RunGraphSolver {
}
public static <S> Optional<EquilibriumStrategy<S>> solve(RunGraph<S> graph) {
Set<RunState<S>> states = new HashSet<>(graph.initialStates());
Queue<RunState<S>> queue = new ArrayDeque<>(states);
while (!queue.isEmpty()) {
graph.successors(queue.poll()).forEach(s -> {
if (states.add(s)) {
queue.add(s);
}
});
}
System.out.println(states.size());
var path = RunGraphSccSolver.searchShort(graph);
if (path.isEmpty()) {
return Optional.empty();
}
AcceptingLasso<S> lasso = new AcceptingLasso<>(path);
Iterator<RunGraph.RunState<S>> iterator = lasso.states(true).iterator();
Iterator<RunState<S>> iterator = lasso.states(true).iterator();
var current = iterator.next();
var suspectGame = graph.suspectGame();
assert current.historyState().equals(suspectGame.initialState().historyState());
assert iterator.hasNext();
// Construct the sequence of moves to obtain the lasso
Map<RunGraph.RunState<S>, Move> runGraphMoves = new HashMap<>();
Map<RunGraph.RunState<S>, DeviationSolver.PunishmentStrategy<S>> punishmentStrategy = new HashMap<>();
Map<RunState<S>, Move> runGraphMoves = new HashMap<>();
Map<RunState<S>, DeviationSolver.PunishmentStrategy<S>> punishmentStrategy = new HashMap<>();
while (iterator.hasNext()) {
var next = iterator.next();
// TODO Bit ugly, could maybe store this information when constructing the lasso
......
......@@ -4,6 +4,7 @@ import com.cges.graph.HistoryGame.HistoryState;
import com.cges.model.Agent;
import com.cges.model.Move;
import com.cges.model.Transition;
import com.google.common.collect.HashMultimap;
import com.google.common.collect.ImmutableSetMultimap;
import com.google.common.collect.SetMultimap;
import com.google.common.collect.Sets;
......@@ -24,7 +25,7 @@ public final class SuspectGame<S> {
private final HistoryGame<S> game;
private final EveState<S> initialState;
private final Map<EveState<S>, SetMultimap<AdamState<S>, EveState<S>>> transitions = new HashMap<>();
private final Map<EveState<S>, Map<AdamState<S>, Set<EveState<S>>>> transitions = new HashMap<>();
public SuspectGame(HistoryGame<S> game) {
this.game = game;
......@@ -36,7 +37,8 @@ public final class SuspectGame<S> {
}
public Stream<SuspectTransition<S>> transitions(EveState<S> eveState) {
return transitions.computeIfAbsent(eveState, this::computeSuccessorMap).entries().stream().map(SuspectTransition::new);
return transitions.computeIfAbsent(eveState, this::computeSuccessorMap).entrySet().stream()
.flatMap(entry -> entry.getValue().stream().map(eve -> new SuspectTransition<>(entry.getKey(), eve)));
}
public Stream<AdamState<S>> successors(EveState<S> eveState) {
......@@ -48,62 +50,92 @@ public final class SuspectGame<S> {
}
public Stream<EveState<S>> eveSuccessors(EveState<S> eveState) {
return transitions.computeIfAbsent(eveState, this::computeSuccessorMap).values().stream();
return transitions.computeIfAbsent(eveState, this::computeSuccessorMap).values().stream().flatMap(Collection::stream);
}
private SetMultimap<AdamState<S>, EveState<S>> computeSuccessorMap(EveState<S> eveState) {
private Map<AdamState<S>, Set<EveState<S>>> computeSuccessorMap(EveState<S> eveState) {
var gameState = eveState.historyState();
if (eveState.suspects().isEmpty()) {
return game.transitions(gameState).collect(Collectors.toUnmodifiableMap(
t -> new AdamState<>(eveState, Set.of(t.move())),
t -> Set.of(new EveState<>(t.destination(), Set.of()))
));
}
var nonSuspects = Set.copyOf(Sets.difference(game.concurrentGame().agents(), eveState.suspects()));
var movesToSuccessors = game.transitions(eveState.historyState())
.collect(ImmutableSetMultimap.toImmutableSetMultimap(Transition::destination, Transition::move));
var nonSuspects = Set.copyOf(Sets.difference(game.concurrentGame().agents(), eveState.suspects()));
assert movesToSuccessors.entries().stream().anyMatch(e ->
game.transition(eveState.historyState(), e.getValue()).orElseThrow().destination().equals(e.getKey()));
// TODO This is somewhat inefficient, but smaller than the subsequent algorithmic problems
// Which set of states can we reach by deviating from the move
SetMultimap<Set<EveState<S>>, Move> reachableByDeviation = HashMultimap.create();
// TODO This is somewhat inefficient, but this is much smaller than the subsequent algorithmic problems
ImmutableSetMultimap.Builder<AdamState<S>, EveState<S>> transitions = ImmutableSetMultimap.builder();
game.transitions(gameState).forEach(transition -> {
var adamSuccessor = new AdamState<>(eveState, transition.move());
game.transitions(gameState).forEach(proposedTransition -> {
// Eve proposes this transition -- adam can either comply or change the choice of one suspect
Move proposedMove = proposedTransition.move();
Collection<Agent> currentSuspects = eveState.suspects();
assert !currentSuspects.isEmpty();
assert movesToSuccessors.get(proposedTransition.destination()).contains(proposedMove);
Set<EveState<S>> deviationSuccessors = new HashSet<>();
// Check for each successor if we can reach it by a single deviation
game.transitions(eveState.historyState()).map(Transition::destination).forEach(alternativeSuccessor -> {
Set<Move> movesLeadingToAlternative = movesToSuccessors.get(alternativeSuccessor);
assert !alternativeSuccessor.equals(proposedTransition.destination()) || movesLeadingToAlternative.contains(proposedMove);
game.transitions(eveState.historyState()).map(Transition::destination).distinct().forEach(historySuccessor -> {
Set<Move> gameMoves = movesToSuccessors.get(historySuccessor);
Collection<Agent> successorSuspects;
if (gameMoves.contains(adamSuccessor.move())) {
if (movesLeadingToAlternative.contains(proposedMove)) {
// Nobody needs to deviate to achieve this move
successorSuspects = currentSuspects;
} else {
successorSuspects = new HashSet<>();
for (Move move : gameMoves) {
if (nonSuspects.stream().allMatch(a -> move.action(a).equals(adamSuccessor.move().action(a)))) {
for (Move move : movesLeadingToAlternative) {
if (nonSuspects.stream().allMatch(a -> move.action(a).equals(proposedMove.action(a)))) {
// Check if there is a single suspect who could deviate to achieve this move (i.e. move to the successor)
var deviatingAgents = currentSuspects.stream()
.filter(a -> !adamSuccessor.move().action(a).equals(move.action(a)))
.iterator();
var deviatingAgents = currentSuspects.stream().filter(a -> !move.action(a).equals(proposedMove.action(a))).iterator();
Agent deviating = null;
if (deviatingAgents.hasNext()) {
Agent deviating = deviatingAgents.next();
var first = deviatingAgents.next();
if (!deviatingAgents.hasNext()) {
successorSuspects.add(deviating);
deviating = first;
}
}
if (deviating != null) {
successorSuspects.add(deviating);
}
assert (game.concurrentGame().agents().stream().filter(a -> !move.action(a).equals(proposedMove.action(a))).count() == 1)
== (deviating != null);
}
}
}
assert currentSuspects.containsAll(successorSuspects);
if (!successorSuspects.isEmpty()) {
transitions.put(adamSuccessor, new EveState<>(historySuccessor, Set.copyOf(successorSuspects)));
deviationSuccessors.add(new EveState<>(alternativeSuccessor, Set.copyOf(successorSuspects)));
}
});
assert deviationSuccessors.stream().map(EveState::historyState).anyMatch(proposedTransition.destination()::equals);
reachableByDeviation.put(Set.copyOf(deviationSuccessors), proposedTransition.move());
});
var built = transitions.build();
assert built.values().stream()
Map<AdamState<S>, Set<EveState<S>>> transitions = reachableByDeviation.asMap().entrySet().stream()
.collect(Collectors.toUnmodifiableMap(e -> new AdamState<>(eveState, Set.copyOf(e.getValue())), Map.Entry::getKey));
assert transitions.values().stream()
.flatMap(Collection::stream)
.map(EveState::suspects)
.flatMap(Collection::stream)
.collect(Collectors.toSet()).equals(eveState.suspects()) : "Vanishing suspects";
assert built.values().stream()
assert transitions.values().stream()
.flatMap(Collection::stream)
.map(EveState::historyState)
.collect(Collectors.toSet())
.containsAll(game.transitions(eveState.historyState()).map(Transition::destination).collect(Collectors.toSet()));
return built;
.containsAll(game.transitions(eveState.historyState()).map(Transition::destination).collect(Collectors.toSet())) :
"Missing successors";
return Map.copyOf(transitions);
}
public HistoryGame<S> historyGame() {
......@@ -112,26 +144,26 @@ public final class SuspectGame<S> {
public static final class AdamState<S> {
private final EveState<S> eveState;
private final Move move;
private final Set<Move> moves;
private final int hashCode;
public AdamState(EveState<S> eveState, Move move) {
public AdamState(EveState<S> eveState, Set<Move> moves) {
this.eveState = eveState;
this.move = move;
this.hashCode = eveState.hashCode() ^ move.hashCode();
this.moves = Set.copyOf(moves);
this.hashCode = eveState.hashCode() ^ Set.copyOf(moves).hashCode();
}
@Override
public String toString() {
return "AS[%s]@[%s]".formatted(eveState.historyState(), move);
return "AS[%s]@[%s]".formatted(eveState.historyState(), moves);
}
public EveState<S> eveState() {
return eveState;
}
public Move move() {
return move;
public Set<Move> moves() {
return moves;
}
@Override
......@@ -140,7 +172,7 @@ public final class SuspectGame<S> {
|| (obj instanceof SuspectGame.AdamState<?> that
&& hashCode == that.hashCode
&& eveState.equals(that.eveState)
&& move.equals(that.move));
&& moves.equals(that.moves));
}
@Override
......
......@@ -10,4 +10,9 @@ public record Transition<S>(Move move, S destination) {
public <T> Transition<T> withDestination(T destination) {
return new Transition<>(move, destination);
}
@Override
public String toString() {
return move + " -> " + destination;
}
}
......@@ -100,15 +100,17 @@ public final class DotWriter {
SuspectGame.EveState<S> eveState = entry.getKey();
game.successors(eveState).forEach(adamState -> {
var compliantTransition = game.historyGame().transition(eveState.historyState(), adamState.move()).orElseThrow();
game.successors(adamState).forEach(eveSuccessor -> {
if (eveSuccessor.historyState().equals(compliantTransition.destination())) {
assert compliantTransition.move().equals(adamState.move());
compliantMoves.put(eveSuccessor, compliantTransition.move());
} else {
deviatingMovesBySuccessor.put(eveSuccessor, adamState.move());
}
});
for (Move move : adamState.moves()) {
var compliantTransition = game.historyGame().transition(eveState.historyState(), move).orElseThrow();
game.successors(adamState).forEach(eveSuccessor -> {
if (eveSuccessor.historyState().equals(compliantTransition.destination())) {
assert compliantTransition.move().equals(adamState.moves());
compliantMoves.put(eveSuccessor, compliantTransition.move());
} else {
deviatingMovesBySuccessor.put(eveSuccessor, move);
}
});
}
});
assert !compliantMoves.isEmpty();
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment