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

Printing of punishment strategies

parent 952af6d0
{
"name": "multipunish",
"type": "explicit",
"ap": [
"s1",
"s2",
"s5",
"s7"
],
"goal": "true",
"agents": {
"A1": {
"goal": "F G s1",
"payoff": "?",
"actions": [
"a",
"b"
]
},
"A2": {
"goal": "F G s5 | F G s7",
"payoff": "?",
"actions": [
"a",
"b"
]
},
"A3": {
"goal": "F G s2 | F G s5",
"payoff": "?",
"actions": [
"a",
"b"
]
}
},
"arena": {
"initial": "s0",
"states": {
"s0": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "a"
},
"to": "s1"
},
{
"actions": {
"A1": "b",
"A2": "a",
"A3": "a"
},
"to": "s2"
},
{
"actions": {
"A1": "a",
"A2": "b",
"A3": "a"
},
"to": "s3"
},
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "b"
},
"to": "s3"
}
]
},
"s1": {
"labels": [
"s1"
],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "a"
},
"to": "s1"
}
]
},
"s2": {
"labels": [
"s2"
],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "a"
},
"to": "s2"
}
]
},
"s3": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "a"
},
"to": "s4"
},
{
"actions": {
"A1": "b",
"A2": "b",
"A3": "a"
},
"to": "s5"
},
{
"actions": {
"A1": "a",
"A2": "b",
"A3": "a"
},
"to": "s6"
}
]
},
"s4": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "a"
},
"to": "s4"
}
]
},
"s5": {
"labels": [
"s5"
],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "a"
},
"to": "s5"
}
]
},
"s6": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "a"
},
"to": "s7"
},
{
"actions": {
"A1": "b",
"A2": "b",
"A3": "b"
},
"to": "s8"
}
]
},
"s7": {
"labels": [
"s7"
],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "a"
},
"to": "s7"
}
]
},
"s8": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a",
"A3": "a"
},
"to": "s8"
}
]
}
}
}
}
\ No newline at end of file
......@@ -82,6 +82,9 @@ public final class Main {
System.out.println("Overall: " + overall);
for (GameSolution<?> gameSolution : list) {
DotWriter.writeSolution(gameSolution, System.out);
System.out.println();
System.out.println();
System.out.println();
}
list.sort(Comparator.comparingLong(solution -> game.agents().stream().map(solution.assignment()::isLoser).count()));
list.stream().map(solution -> Formatter.format(solution.assignment(), game)).forEach(System.out::println);
......
package com.cges.algorithm;
import static com.google.common.base.Preconditions.checkArgument;
import com.cges.graph.HistoryGame;
import com.cges.graph.HistoryGame.HistoryState;
import com.cges.graph.SuspectGame;
......@@ -20,12 +18,12 @@ import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Optional;
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;
......@@ -40,7 +38,7 @@ import owl.ltl.rewriter.SimplifierRepository;
import owl.translations.LtlTranslationRepository;
import owl.translations.LtlTranslationRepository.Option;
public final class DeviationSolver<S> {
public final class DeviationSolver<S> implements PunishmentStrategy<S> {
private static final boolean CROSS_VALIDATE = false;
private static final Function<LabelledFormula, Automaton<?, ? extends ParityAcceptance>> translation =
......@@ -63,6 +61,8 @@ public final class DeviationSolver<S> {
private final Map<HistoryState<S>, Boolean> isWinning;
private final Map<HistoryState<S>, 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 ->
......@@ -92,12 +92,13 @@ public final class DeviationSolver<S> {
isWinning = Map.of();
strategy = Map.of();
initialStates = Map.of();
game = null;
} else {
var gameSolution = solveParityGame(eveState, goal);
var parityGame = gameSolution.parityGame();
game = gameSolution.parityGame();
var paritySolution = gameSolution.solution();
Set<PriorityState<S>> solvedTopLevelEveStates = parityGame.states().stream()
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<>();
......@@ -108,8 +109,8 @@ public final class DeviationSolver<S> {
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);
if (game.owner(next) == Player.EVEN) {
successors = game.successors(next);
} else {
PriorityState<S> successor = paritySolution.oddStrategy().get(next);
strategy.put(next, successor);
......@@ -144,30 +145,17 @@ public final class DeviationSolver<S> {
.map(a -> Conjunction.of(GOperator.of(agentLiterals.get(a)), historyState.goal(a)))).not(), atomicPropositions);
}
private Optional<PunishmentStrategy<S>> doSolve(HistoryState<S> historyState) {
public boolean isWinning(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));
}
assert computeWinning(historyState) == ((BooleanConstant) goal).value;
winning = ((BooleanConstant) goal).value;
}
return Optional.empty();
}
public Optional<PunishmentStrategy<S>> solve(HistoryState<S> historyState) {
var solution = doSolve(historyState);
assert computeWinning(historyState) == solution.isPresent();
return solution;
assert winning == computeWinning(historyState);
return winning;
}
private boolean computeWinning(HistoryState<S> historyState) {
......@@ -175,6 +163,25 @@ public final class DeviationSolver<S> {
return solution.solution().winner(solution.parityGame().initialState()) == Player.ODD;
}
@Override
public PriorityState<S> initialState(HistoryState<S> state) {
return initialStates.get(state);
}
@Override
public PriorityState<S> move(PriorityState<S> state) {
assert state.isEve();
return strategy.getOrDefault(state, state);
}
@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());
}
record ParitySolution<S>(SuspectParityGame<S> parityGame, Solution<PriorityState<S>> solution) {}
private ParitySolution<S> solveParityGame(EveState<S> eveState, LabelledFormula goal) {
......@@ -185,18 +192,4 @@ public final class DeviationSolver<S> {
var paritySolution = solver.solve(parityGame);
return new ParitySolution<>(parityGame, paritySolution);
}
public interface PunishmentStrategy<S> {
PriorityState<S> initialState();
PriorityState<S> move(PriorityState<S> state);
}
record Strategy<S>(PriorityState<S> initialState, Map<PriorityState<S>, PriorityState<S>> strategies) implements PunishmentStrategy<S> {
@Override
public PriorityState<S> move(PriorityState<S> state) {
checkArgument(strategies.containsKey(state));
return strategies.get(state);
}
}
}
package com.cges.algorithm;
import com.cges.graph.HistoryGame;
import com.cges.parity.PriorityState;
import java.util.Set;
public interface PunishmentStrategy<S> {
PriorityState<S> initialState(HistoryGame.HistoryState<S> state);
PriorityState<S> move(PriorityState<S> state);
Set<PriorityState<S>> successors(PriorityState<S> state);
}
......@@ -72,7 +72,6 @@ public final class RunGraphSolver {
// Construct the sequence of moves to obtain the lasso
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
......@@ -83,10 +82,9 @@ public final class RunGraphSolver {
runGraphMoves.put(current, move);
// For each deviation, provide a proof that we can punish someone
punishmentStrategy.put(current, graph.deviationStrategy(current.historyState()));
current = next;
}
var strategy = new EquilibriumStrategy<>(lasso, Map.copyOf(runGraphMoves), Map.copyOf(punishmentStrategy));
var strategy = new EquilibriumStrategy<>(lasso, Map.copyOf(runGraphMoves), graph.deviationStrategy());
assert validate(strategy, graph);
return Optional.of(strategy);
}
......
package com.cges.graph;
import com.cges.algorithm.DeviationSolver;
import com.cges.algorithm.PunishmentStrategy;
import com.cges.graph.HistoryGame.HistoryState;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
......@@ -13,7 +14,6 @@ import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.Optional;
import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;
......@@ -38,7 +38,6 @@ public final class RunGraph<S> {
private final SuspectGame<S> suspectGame;
private final Map<S, BitSet> labelCache = new HashMap<>();
private final Map<String, Integer> propositionIndex;
private final Map<HistoryState<S>, Optional<DeviationSolver.PunishmentStrategy<S>>> historySolutions = new HashMap<>();
private final DeviationSolver<S> deviationSolver;
private final HistoryGame<S> historyGame;
......@@ -67,7 +66,7 @@ public final class RunGraph<S> {
}
public Set<RunState<S>> initialStates() {
if (isWinning(historyGame.initialState())) {
if (deviationSolver.isWinning(historyGame.initialState())) {
return automaton.initialStates().stream()
.map(s -> new RunState<>(s, historyGame.initialState()))
.collect(Collectors.toSet());
......@@ -75,12 +74,8 @@ public final class RunGraph<S> {
return Set.of();
}
public boolean isWinning(HistoryState<S> historyState) {
return historySolutions.computeIfAbsent(historyState, deviationSolver::solve).isPresent();
}
public DeviationSolver.PunishmentStrategy<S> deviationStrategy(HistoryState<S> historyState) {
return historySolutions.computeIfAbsent(historyState, deviationSolver::solve).orElseThrow();
public PunishmentStrategy<S> deviationStrategy() {
return deviationSolver;
}
private BitSet labels(RunState<S> current) {
......@@ -100,7 +95,7 @@ public final class RunGraph<S> {
return Set.of();
}
var transitions = historyGame.transitions(current.historyState())
.filter(t -> isWinning(t.destination()))
.filter(t -> deviationSolver.isWinning(t.destination()))
.flatMap(transition -> automatonEdges.stream().map(edge ->
new RunTransition<>(new RunState<>(edge.successor(), transition.destination()), !edge.colours().isEmpty())))
.collect(Collectors.toSet());
......
......@@ -4,33 +4,49 @@ import static com.google.common.base.Preconditions.checkArgument;
import com.cges.graph.RunGraph.RunState;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import javax.annotation.Nullable;
public class AcceptingLasso<S> {
private final List<RunState<S>> transientStates;
private final List<RunState<S>> loopStates;
private final Map<RunState<S>, RunState<S>> successors;
public AcceptingLasso(List<RunState<S>> loop) {
List<RunState<S>> transientStates = new ArrayList<>();
List<RunState<S>> loopStates = new ArrayList<>();
Map<RunState<S>, RunState<S>> successors = new HashMap<>();
RunState<S> backLink = loop.get(loop.size() - 1);
boolean inLoop = false;
for (RunState<S> state : loop.subList(0, loop.size() - 1)) {
List<RunState<S>> states = loop.subList(0, loop.size() - 1);
var iterator = states.iterator();
@Nullable
RunState<S> previous = null;
while (iterator.hasNext()) {
RunState<S> state = iterator.next();
if (!inLoop && state.equals(backLink)) {
inLoop = true;
}
if (previous != null) {
successors.put(previous, state);
}
if (inLoop) {
loopStates.add(state);
} else {
transientStates.add(state);
}
previous = state;
}
successors.put(previous, backLink);
checkArgument(inLoop);
this.transientStates = List.copyOf(transientStates);
this.loopStates = List.copyOf(loopStates);
this.successors = Map.copyOf(successors);
}
public Stream<RunState<S>> transientStates() {
......@@ -45,6 +61,10 @@ public class AcceptingLasso<S> {
return Stream.concat(transientStates(), loopStates(withClosingState));
}
public RunState<S> successor(RunState<S> state) {
return successors.get(state);
}
public int size() {
return transientStates.size() + loopStates.size();
}
......
package com.cges.model;
import com.cges.algorithm.PunishmentStrategy;
import com.cges.graph.RunGraph;
import com.cges.algorithm.DeviationSolver;
import java.util.Map;
import java.util.stream.Collectors;
public record EquilibriumStrategy<S>(AcceptingLasso<S> lasso, Map<RunGraph.RunState<S>, Move> moves,
Map<RunGraph.RunState<S>, DeviationSolver.PunishmentStrategy<S>> punishmentStrategies) {
PunishmentStrategy<S> punishmentStrategy) {
@Override
public String toString() {
return "TRANSIENT" + lasso.transientStates().map(state -> state + "->" + moves.get(state)).collect(Collectors.joining("\n", "\n", "\n"))
......
......@@ -11,15 +11,17 @@ import com.cges.model.ConcurrentGame;
import com.cges.model.Move;
import com.cges.parity.ParityGame;
import com.cges.parity.Player;
import com.cges.parity.PriorityState;
import com.cges.parser.Module;
import com.cges.parser.ModuleGame;
import com.google.common.collect.HashMultimap;
import com.google.common.collect.SetMultimap;
import com.google.common.collect.Sets;
import it.unimi.dsi.fastutil.objects.Object2IntMap;
import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap;
import java.io.PrintStream;
import java.util.ArrayDeque;
import java.util.Collection;
import java.util.Comparator;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
......@@ -214,7 +216,7 @@ public final class DotWriter {
writer.append("}");
}
public static <S> void writeSolution(GameSolution<S> solution, PrintStream writer) {
public static <S> void writeLasso(GameSolution<S> solution, PrintStream writer) {
var suspectGame = solution.suspectGame();
var strategy = solution.strategy();
var runGraph = solution.runGraph();
......@@ -222,20 +224,11 @@ public final class DotWriter {
writer.append("digraph {\n");
Set<RunGraph.RunState<S>> loopStates = strategy.lasso().states(false).collect(Collectors.toSet());
Set<RunGraph.RunState<S>> successors = Set.of();
/*
Set<RunGraph.RunState<S>> successors = loopStates.stream().map(runGraph::transitions)
.flatMap(Collection::stream)
.map(RunGraph.RunTransition::successor)
.filter(s -> !loopStates.contains(s))
.collect(Collectors.toSet());
*/
Object2IntMap<RunGraph.RunState<S>> ids = new Object2IntOpenHashMap<>();
ids.defaultReturnValue(-1);
Sets.union(loopStates, successors).forEach(runState -> ids.put(runState, ids.size()));
Sets.union(loopStates, successors).forEach(runState -> {
int id = ids.getInt(runState);
loopStates.forEach(runState -> ids.put(runState, ids.size()));
ids.forEach((runState, id) -> {
HistoryState<S> historyState = runState.historyState();
String label = Stream.concat(Stream.concat(Stream.of(DotFormatted.toRecordString(DotFormatted.toString(historyState.state()))),
suspectGame.historyGame().concurrentGame().agents().stream()
......@@ -247,24 +240,92 @@ public final class DotWriter {
.collect(Collectors.joining("|", "{", "}"));
writer.append("S_%d [shape=record,label=\"%s\"]\n".formatted(id, label));
});
strategy.lasso().states(false).forEach(runState -> {
int id = ids.getInt(runState);
ids.forEach((runState, id) -> {
Move move = strategy.moves().get(runState);
var historySuccessor = suspectGame.historyGame().transition(runState.historyState(), move).orElseThrow().destination();
var runSuccessor = runGraph.successors(runState).stream().filter(s -> s.historyState().equals(historySuccessor)).findAny()
var runSuccessor = runGraph.successors(runState).stream()
.filter(s -> s.historyState().equals(historySuccessor)).findAny()