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

Snapshot

parent b34dd76e
......@@ -62,7 +62,7 @@ configurations {
application {
mainClass.set("com.cges.Main")
// applicationDefaultJvmArgs = listOf("-ea")
applicationDefaultJvmArgs = listOf("-ea")
}
tasks.generateGrammarSource {
......
package com.cges;
import com.cges.algorithm.FormulaHistoryGame;
import com.cges.algorithm.HistoryGame;
import com.cges.algorithm.RunGraph;
import com.cges.algorithm.RunGraphSccSolver;
import com.cges.algorithm.StrategyMapper;
......@@ -53,7 +54,7 @@ public final class Main {
}
analyse(game).forEach(solution -> System.out.printf("Found NE for %s:%n%s%n",
Formatter.format(solution.assignment(), game),
solution.strategy().lasso()));
solution.strategy()));
System.out.println("Overall: " + overall);
}
......@@ -73,9 +74,13 @@ public final class Main {
var suspectSolution = SuspectSolver.computeReachableWinningEveStates(suspectGame, payoff);
System.out.println("Winning: " + winningStopwatch);
Set<HistoryGame.HistoryState<S>> winningHistoryStates = suspectSolution.winningStates().stream()
.filter(eve -> eve.suspects().equals(game.agents()))
.map(SuspectGame.EveState::historyState)
.collect(Collectors.toSet());
Stopwatch solutionStopwatch = Stopwatch.createStarted();
var runGraph = RunGraph.create(suspectGame.historyGame(), payoff,
state -> suspectSolution.isWinning(new SuspectGame.EveState<>(state, game.agents())));
var runGraph = RunGraph.create(suspectGame.historyGame(), payoff, winningHistoryStates::contains);
var lasso = RunGraphSccSolver.solve(runGraph);
System.out.println("Solution: " + solutionStopwatch);
if (lasso.isPresent()) {
......@@ -84,8 +89,7 @@ public final class Main {
} else {
return Optional.empty();
}
})
.flatMap(Optional::stream);
}).flatMap(Optional::stream);
}
record GameSolution<S>(PayoffAssignment assignment, EquilibriumStrategy<S> strategy) {}
......
......@@ -5,14 +5,19 @@ import static com.google.common.base.Preconditions.checkArgument;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.Transition;
import com.google.common.collect.Lists;
import com.google.common.collect.ImmutableSetMultimap;
import com.google.common.collect.SetMultimap;
import de.tum.in.naturals.Indices;
import java.util.ArrayDeque;
import java.util.Arrays;
import java.util.BitSet;
import java.util.Comparator;
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.stream.Collectors;
import java.util.stream.Stream;
......@@ -23,19 +28,23 @@ import owl.ltl.Formula;
public class FormulaHistoryGame<S> implements HistoryGame<S> {
static final class ListHistoryState<S> implements HistoryState<S> {
private static final EquivalenceClass[] EMPTY = new EquivalenceClass[0];
private final S state;
private final List<EquivalenceClass> agentGoals;
private final EquivalenceClass[] agentGoals;
private final Map<Agent, Integer> agentIndices;
private final int hashCode;
ListHistoryState(S state, List<EquivalenceClass> agentGoals, Map<Agent, Integer> agentIndices) {
this.state = state;
this.agentGoals = List.copyOf(agentGoals);
this.agentGoals = agentGoals.toArray(EMPTY);
this.agentIndices = Map.copyOf(agentIndices);
this.hashCode = this.state.hashCode() ^ Arrays.hashCode(this.agentGoals);
}
@Override
public Formula goal(Agent agent) {
return agentGoals.get(agentIndices.get(agent)).canonicalRepresentative();
return agentGoals[agentIndices.get(agent)].canonicalRepresentative();
}
@Override
......@@ -44,27 +53,28 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
}
public List<EquivalenceClass> agentGoals() {
return agentGoals;
return Arrays.asList(agentGoals);
}
@Override
public boolean equals(Object obj) {
return obj == this
|| (obj instanceof ListHistoryState<?> that
&& Objects.equals(this.state, that.state)
&& Objects.equals(this.agentGoals, that.agentGoals));
&& hashCode == that.hashCode
&& Arrays.equals(agentGoals, that.agentGoals)
&& state.equals(that.state));
}
@Override
public int hashCode() {
return state.hashCode() ^ agentGoals.hashCode();
return hashCode;
}
@Override
public String toString() {
return state + "@" + agentIndices.entrySet().stream().sorted(Map.Entry.comparingByKey(Comparator.comparing(Agent::name)))
.map(Map.Entry::getValue)
.map(agentGoals::get)
.map(i -> agentGoals[i])
.map(EquivalenceClass::canonicalRepresentative)
.map(Objects::toString)
.collect(Collectors.joining(",", "[", "]"));
......@@ -72,9 +82,8 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
}
private final ConcurrentGame<S> game;
private final Map<String, Integer> propositionIndices;
private final Map<Agent, Integer> agentIndices;
private final HistoryState<S> initialState;
private final ListHistoryState<S> initialState;
private final SetMultimap<HistoryState<S>, Transition<HistoryState<S>>> transitions;
public FormulaHistoryGame(ConcurrentGame<S> game) {
this.game = game;
......@@ -82,18 +91,45 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
Map<String, Integer> propositionIndices = new HashMap<>();
Indices.forEachIndexed(game.atomicPropositions(), (index, proposition) -> propositionIndices.put(proposition, index));
this.propositionIndices = Map.copyOf(propositionIndices);
Map<Agent, Integer> agentIndices = new HashMap<>();
Indices.forEachIndexed(game.agents(), (index, agent) -> agentIndices.put(agent, index));
this.agentIndices = Map.copyOf(agentIndices);
Map<Agent, Integer> indices = Map.copyOf(agentIndices);
this.initialState = new ListHistoryState<>(game.initialState(),
game.agents().stream().map(Agent::goal).map(factory::of).toList(),
agentIndices);
game.agents().stream().map(Agent::goal).map(factory::of).map(EquivalenceClass::unfold).toList(), indices);
ImmutableSetMultimap.Builder<HistoryState<S>, Transition<HistoryState<S>>> transitions = ImmutableSetMultimap.builder();
Set<ListHistoryState<S>> states = new HashSet<>(List.of(initialState));
Queue<ListHistoryState<S>> queue = new ArrayDeque<>(states);
Map<S, BitSet> labelCache = new HashMap<>();
while (!queue.isEmpty()) {
ListHistoryState<S> state = queue.poll();
BitSet valuation = labelCache.computeIfAbsent(state.state(), s -> {
BitSet set = new BitSet();
game.labels(s).stream().map(propositionIndices::get).forEach(set::set);
return set;
});
List<EquivalenceClass> successorGoals = state.agentGoals().stream()
.map(f -> f.temporalStep(valuation).unfold())
.toList();
var successors = game.transitions(state.state())
.map(transition -> transition.withDestination((HistoryState<S>)
new ListHistoryState<>(transition.destination(), successorGoals, indices)))
.collect(Collectors.toSet());
transitions.putAll(state, successors);
for (Transition<HistoryState<S>> transition : successors) {
var successor = (ListHistoryState<S>) transition.destination();
if (states.add(successor)) {
queue.add(successor);
}
}
}
this.transitions = transitions.build();
}
@Override
public HistoryState<S> initialState() {
public ListHistoryState<S> initialState() {
return initialState;
}
......@@ -101,12 +137,7 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
public Stream<Transition<HistoryState<S>>> transitions(HistoryState<S> state) {
checkArgument(state instanceof FormulaHistoryGame.ListHistoryState<S>);
ListHistoryState<S> history = (ListHistoryState<S>) state;
Set<String> labels = game.labels(state.state());
BitSet valuation = new BitSet();
labels.stream().map(propositionIndices::get).forEach(valuation::set);
List<EquivalenceClass> successorGoals = Lists.transform(history.agentGoals(), f -> f.unfold().temporalStep(valuation));
return game.transitions(state.state())
.map(transition -> transition.withDestination(new ListHistoryState<>(transition.destination(), successorGoals, agentIndices)));
return transitions.get(history).stream();
}
@Override
......
package com.cges.algorithm;
import com.cges.algorithm.HistoryGame.HistoryState;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.PayoffAssignment;
......@@ -36,7 +37,7 @@ public final class RunGraph<S> {
private static final Logger logger = Logger.getLogger(RunGraph.class.getName());
public static <S> RunGraph<S> create(HistoryGame<S> historyGame, PayoffAssignment payoffAssignment,
Predicate<HistoryGame.HistoryState<S>> winningHistoryStates) {
Predicate<HistoryState<S>> winningHistoryStates) {
if (!winningHistoryStates.test(historyGame.initialState())) {
return new RunGraph<>(Set.of(), Set.of(), ImmutableSetMultimap.of());
}
......@@ -100,6 +101,7 @@ public final class RunGraph<S> {
}
}
assert states.stream().map(RunState::historyState).allMatch(winningHistoryStates);
logger.log(Level.FINER, () -> "Run graph has %d states, %d initial".formatted(states.size(), initialStates.size()));
return new RunGraph<>(initialStates, states, runGraph.build());
}
......@@ -135,7 +137,7 @@ public final class RunGraph<S> {
return transitions(state).stream().map(Transition::destination).collect(Collectors.toSet());
}
public record RunState<S>(Object automatonState, HistoryGame.HistoryState<S> historyState, boolean accepting) {
public record RunState<S>(Object automatonState, HistoryState<S> historyState, boolean accepting) {
@Override
public String toString() {
return "(%s,%s)%s".formatted(automatonState, historyState, accepting ? "!" : "");
......
package com.cges.algorithm;
import com.cges.algorithm.SuspectGame.EveState;
import com.cges.model.AcceptingLasso;
import com.cges.model.Agent;
import com.cges.model.EquilibriumStrategy;
import com.cges.model.Move;
import com.cges.model.Transition;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
public final class StrategyMapper {
public interface PunishmentStrategy {
}
private StrategyMapper() {}
public static <S> EquilibriumStrategy<S> createStrategy(SuspectGame<S> suspectGame,
SuspectSolver.SuspectSolution<S> suspectSolution, AcceptingLasso<S> lasso) {
public static <S> EquilibriumStrategy<S>
createStrategy(SuspectGame<S> suspectGame, SuspectSolver.SuspectSolution<S> suspectSolution, AcceptingLasso<S> lasso) {
Iterator<RunGraph.RunState<S>> iterator = lasso.states(true).iterator();
var current = iterator.next();
assert current.historyState().equals(suspectGame.initialState().historyState());
assert iterator.hasNext();
Set<Agent> agents = suspectGame.historyGame().concurrentGame().agents();
// Construct the sequence of moves to obtain the lasso
Map<RunGraph.RunState<S>, Move> runGraphMoves = new HashMap<>();
Map<RunGraph.RunState<S>, SuspectSolver.SuspectStrategy<S>> punishmentStrategy = new HashMap<>();
while (iterator.hasNext()) {
var next = iterator.next();
// TODO Bit ugly, could store this information when constructing the lasso
// TODO Bit ugly, could maybe store this information when constructing the lasso
Move move = suspectGame.historyGame().transitions(current.historyState())
.filter(t -> t.destination().equals(next.historyState()))
.map(Transition::move)
.iterator().next();
runGraphMoves.put(current, move);
//
// var eveSuccessors = suspectGame.successors(new SuspectGame.AdamState<S>(current.eveState(), move));
// assert eveSuccessors.contains(next.historyState());
//
// // For each deviation, provide a proof that we can punish someone
// Set<SuspectGame.EveState<S>> deviations = eveSuccessors.stream()
// .filter(state -> !next.eveState().equals(state))
// .collect(Collectors.toSet());
EveState<S> eveState = new EveState<>(current.historyState(), agents);
assert suspectSolution.isWinning(eveState);
// For each deviation, provide a proof that we can punish someone
punishmentStrategy.put(current, suspectSolution.strategy(eveState));
current = next;
}
return new EquilibriumStrategy<>(lasso, Map.copyOf(runGraphMoves), Map.of());
return new EquilibriumStrategy<>(lasso, Map.copyOf(runGraphMoves), Map.copyOf(punishmentStrategy));
}
}
......@@ -135,14 +135,56 @@ public final class SuspectGame<S> {
return game;
}
public record AdamState<S>(EveState<S> eveState, Move move) {
public static final class AdamState<S> {
private final EveState<S> eveState;
private final Move move;
private final int hashCode;
public AdamState(EveState<S> eveState, Move move) {
this.eveState = eveState;
this.move = move;
this.hashCode = eveState.hashCode() ^ move.hashCode();
}
@Override
public String toString() {
return "AS[%s]@[%s]".formatted(eveState.historyState(), move);
}
public EveState<S> eveState() {
return eveState;
}
public Move move() {
return move;
}
@Override
public boolean equals(Object obj) {
return obj == this
|| (obj instanceof SuspectGame.AdamState<?> that
&& hashCode == that.hashCode
&& eveState.equals(that.eveState)
&& move.equals(that.move));
}
@Override
public int hashCode() {
return hashCode;
}
}
public record EveState<S>(HistoryState<S> historyState, Set<Agent> suspects) {
public static final class EveState<S> {
private final HistoryState<S> historyState;
private final Set<Agent> suspects;
private final int hashCode;
public EveState(HistoryState<S> historyState, Set<Agent> suspects) {
this.historyState = historyState;
this.suspects = Set.copyOf(suspects);
this.hashCode = historyState.hashCode() ^ suspects.hashCode();
}
public S gameState() {
return historyState.state();
}
......@@ -151,5 +193,27 @@ public final class SuspectGame<S> {
public String toString() {
return "ES[%s]{%s}".formatted(historyState, suspects.stream().map(Agent::name).sorted().collect(Collectors.joining(",")));
}
public HistoryState<S> historyState() {
return historyState;
}
public Set<Agent> suspects() {
return suspects;
}
@Override
public boolean equals(Object obj) {
return (this == obj)
|| (obj instanceof EveState<?> that
&& hashCode == that.hashCode
&& historyState.equals(that.historyState)
&& suspects.equals(that.suspects));
}
@Override
public int hashCode() {
return hashCode;
}
}
}
......@@ -6,9 +6,9 @@ import com.cges.algorithm.SuspectGame.EveState;
import com.cges.model.Agent;
import com.cges.model.PayoffAssignment;
import com.cges.parity.Player;
import com.cges.parity.oink.LazySuspectParityGame;
import com.cges.parity.oink.OinkGameSolver;
import com.cges.parity.oink.PriorityState;
import com.cges.parity.SuspectParityGame;
import com.cges.parity.OinkGameSolver;
import com.cges.parity.PriorityState;
import java.util.ArrayDeque;
import java.util.Collection;
import java.util.Comparator;
......@@ -170,46 +170,13 @@ public final class SuspectSolver<S> {
minimized.acceptance(minimized.acceptance().withAcceptanceSets(2));
}
MutableAutomatonUtil.complete(minimized, sink);
minimized.trim();
return minimized;
});
if (automaton.size() == 0) {
return Optional.empty();
}
// if (true) {
// var edgeGame = new SuspectEdgeGame<>(game, automaton);
// var solution = new StrategyIterationSolver<>(edgeGame).solve();
//
// if (solution.winner(edgeGame.initialState()) == Player.EVEN) {
// return Optional.empty();
// }
//
// Queue<EdgePriorityState<S>> queue = new ArrayDeque<>(List.of(edgeGame.initialState()));
// Set<EdgePriorityState<S>> reached = new HashSet<>();
// Map<EdgePriorityState<S>, Edge<EdgePriorityState<S>>> strategy = new HashMap<>();
// while (!queue.isEmpty()) {
// EdgePriorityState<S> next = queue.poll();
// assert solution.winner(next) == Player.ODD;
// Stream<Edge<EdgePriorityState<S>>> edges;
// if (edgeGame.owner(next) == Player.EVEN) {
// edges = edgeGame.edges(next);
// } else {
// var solutionEdge = solution.oddStrategy().apply(next).iterator().next();
// strategy.put(next, solutionEdge);
// edges = Stream.of(solutionEdge);
// }
// edges.forEach(edge -> {
// EdgePriorityState<S> successor = edge.successor();
// if (reached.add(successor)) {
// queue.add(successor);
// }
// });
// }
//
// return Optional.of(new Strategy<>(null, Map.of()));
// }
var parityGame = LazySuspectParityGame.create(game, eveState, automaton);
var parityGame = SuspectParityGame.create(game, eveState, automaton);
var paritySolution = solver.solve(parityGame);
if (paritySolution.winner(parityGame.initialState()) == Player.EVEN) {
......
......@@ -2,21 +2,22 @@ package com.cges.model;
import static com.google.common.base.Preconditions.checkArgument;
import com.cges.algorithm.RunGraph;
import com.cges.algorithm.RunGraph.RunState;
import java.util.ArrayList;
import java.util.List;
import java.util.stream.Collectors;
import java.util.stream.Stream;
public class AcceptingLasso<S> {
private final List<RunGraph.RunState<S>> transientStates;
private final List<RunGraph.RunState<S>> loopStates;
private final List<RunState<S>> transientStates;
private final List<RunState<S>> loopStates;
public AcceptingLasso(List<RunGraph.RunState<S>> loop) {
List<RunGraph.RunState<S>> transientStates = new ArrayList<>();
List<RunGraph.RunState<S>> loopStates = new ArrayList<>();
RunGraph.RunState<S> backLink = loop.get(loop.size() - 1);
public AcceptingLasso(List<RunState<S>> loop) {
List<RunState<S>> transientStates = new ArrayList<>();
List<RunState<S>> loopStates = new ArrayList<>();
RunState<S> backLink = loop.get(loop.size() - 1);
boolean inLoop = false;
for (RunGraph.RunState<S> state : loop.subList(0, loop.size() - 1)) {
for (RunState<S> state : loop.subList(0, loop.size() - 1)) {
if (!inLoop && state.equals(backLink)) {
inLoop = true;
}
......@@ -27,25 +28,31 @@ public class AcceptingLasso<S> {
}
}
checkArgument(inLoop);
checkArgument(loopStates.stream().anyMatch(RunGraph.RunState::accepting));
checkArgument(loopStates.stream().anyMatch(RunState::accepting));
this.transientStates = List.copyOf(transientStates);
this.loopStates = List.copyOf(loopStates);
}
public Stream<RunGraph.RunState<S>> transientStates() {
public Stream<RunState<S>> transientStates() {
return transientStates.stream();
}
public Stream<RunGraph.RunState<S>> loopStates(boolean withClosingState) {
public Stream<RunState<S>> loopStates(boolean withClosingState) {
return withClosingState ? Stream.concat(loopStates.stream(), Stream.of(loopStates.get(0))) : loopStates.stream();
}
public Stream<RunGraph.RunState<S>> states(boolean withClosingState) {
public Stream<RunState<S>> states(boolean withClosingState) {
return Stream.concat(transientStates(), loopStates(withClosingState));
}
public int size() {
return transientStates.size() + loopStates.size();
}
@Override
public String toString() {
return transientStates.stream().map(RunState::toString).collect(Collectors.joining(" "))
+ " | " + loopStates.stream().map(RunState::toString).collect(Collectors.joining(" "));
}
}
......@@ -18,6 +18,15 @@ public final class Agent {
case UNDEFINED -> "?";
};
}
public static Payoff parse(String string) {
return switch (string) {
case "1", "true" -> Agent.Payoff.WINNING;
case "0", "false" -> Agent.Payoff.LOSING;
case "?" -> Agent.Payoff.UNDEFINED;
default -> throw new IllegalArgumentException("Unsupported payoff string " + string);
};
}
}
private final String name;
......
package com.cges.model;
import com.cges.algorithm.RunGraph;
import com.cges.algorithm.SuspectGame;
import com.cges.parity.oink.PriorityState;
import com.cges.algorithm.SuspectSolver;
import java.util.Map;
import java.util.stream.Collectors;
public record EquilibriumStrategy<S>(AcceptingLasso<S> lasso, Map<RunGraph.RunState<S>, Move> moves,
Map<SuspectGame.EveState<S>, PunishmentStrategy<S>> punishmentStrategies) {
public record PunishmentStrategy<S>(Map<PriorityState<S>, Move> strategy) {}
Map<RunGraph.RunState<S>, SuspectSolver.SuspectStrategy<S>> punishmentStrategies) {
@Override
public String toString() {
return lasso.states(false).map(state -> state.historyState().state() + "->" + moves.get(state)).collect(Collectors.joining(", "));
}
}
......@@ -7,7 +7,7 @@ import com.cges.model.ConcurrentGame;
import com.cges.model.EquilibriumStrategy;
import com.cges.model.Transition;
import com.cges.parity.Player;
import com.cges.parity.oink.ParityGame;
import com.cges.parity.ParityGame;
import it.unimi.dsi.fastutil.objects.Object2IntMap;
import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap;
import java.io.PrintStream;
......
package com.cges.parity.oink;
package com.cges.parity;
public class OinkExecutionException extends RuntimeException {
public OinkExecutionException(String message) {
......
package com.cges.parity.oink;
package com.cges.parity;
import static com.google.common.base.Preconditions.checkState;
import static java.util.Objects.requireNonNull;
......@@ -35,7 +35,7 @@ public final class OinkGameSolver {
public OinkGameSolver() {}
public <S> ParityGame.Solution<S> solve(ParityGame<S> game) {
public <S> Solution<S> solve(ParityGame<S> game) {