Commit 15f4d0b4 authored by Tobias MEGGENDORFER's avatar Tobias MEGGENDORFER
Browse files

Snap

parent c6e956a7
{
"name": "example",
"ap": [
"s1",
"s2"
],
"agents": {
"A1": {
"goal": "F G s1",
"payoff": "?",
"actions": [
"a",
"b"
]
},
"A2": {
"goal": "F G s2",
"payoff": "?",
"actions": [
"c",
"d"
]
}
},
"arena": {
"initial": "s0",
"states": {
"s0": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "c"
},
"to": "s0"
},
{
"actions": {
"A1": "b",
"A2": "c"
},
"to": "s1"
}
]
},
"s1": {
"labels": [
"s1"
],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "c"
},
"to": "s1"
},
{
"actions": {
"A1": "a",
"A2": "d"
},
"to": "s2"
}
]
},
"s2": {
"labels": [
"s2"
],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "c"
},
"to": "s2"
}
]
}
}
}
}
\ No newline at end of file
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;
......@@ -71,16 +70,11 @@ public final class Main {
.peek(p -> System.out.printf("Processing: %s%n", Formatter.format(p, game)))
.<Optional<GameSolution<S>>>map(payoff -> {
Stopwatch winningStopwatch = Stopwatch.createStarted();
var suspectSolution = SuspectSolver.computeReachableWinningEveStates(suspectGame, payoff);
var suspectSolution = SuspectSolver.computeReachableWinningStates(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, winningHistoryStates::contains);
var runGraph = RunGraph.create(suspectGame.historyGame(), payoff, suspectSolution::isWinning);
var lasso = RunGraphSccSolver.solve(runGraph);
System.out.println("Solution: " + solutionStopwatch);
if (lasso.isPresent()) {
......
package com.cges.algorithm;
import static com.google.common.base.Preconditions.checkArgument;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.Transition;
......@@ -111,7 +109,7 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
return set;
});
List<EquivalenceClass> successorGoals = state.agentGoals().stream()
.map(f -> f.temporalStep(valuation).unfold())
.map(goal -> goal.temporalStep(valuation).unfold())
.toList();
var successors = game.transitions(state.state())
.map(transition -> transition.withDestination((HistoryState<S>)
......@@ -135,9 +133,7 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
@Override
public Stream<Transition<HistoryState<S>>> transitions(HistoryState<S> state) {
checkArgument(state instanceof FormulaHistoryGame.ListHistoryState<S>);
ListHistoryState<S> history = (ListHistoryState<S>) state;
return transitions.get(history).stream();
return transitions.get(state).stream();
}
@Override
......
......@@ -6,13 +6,8 @@ import com.cges.model.Transition;
import java.util.stream.Stream;
import owl.ltl.Formula;
public class MockHistoryGame<S> implements HistoryGame<S> {
public record MockHistoryGame<S>(ConcurrentGame<S> concurrentGame) implements HistoryGame<S> {
record MockHistoryState<S>(S state) implements HistoryGame.HistoryState<S> {
@Override
public S state() {
return state;
}
@Override
public Formula goal(Agent agent) {
return agent.goal();
......@@ -24,24 +19,13 @@ public class MockHistoryGame<S> implements HistoryGame<S> {
}
}
private final ConcurrentGame<S> game;
public MockHistoryGame(ConcurrentGame<S> game) {
this.game = game;
}
@Override
public HistoryState<S> initialState() {
return new MockHistoryState<>(this.game.initialState());
return new MockHistoryState<>(this.concurrentGame.initialState());
}
@Override
public Stream<Transition<HistoryState<S>>> transitions(HistoryState<S> state) {
return game.transitions(state.state()).map(transition -> transition.withDestination(new MockHistoryState<>(transition.destination())));
}
@Override
public ConcurrentGame<S> concurrentGame() {
return game;
return concurrentGame.transitions(state.state()).map(Transition.transform(MockHistoryState::new));
}
}
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;
......@@ -15,7 +14,7 @@ public final class StrategyMapper {
private StrategyMapper() {}
public static <S> EquilibriumStrategy<S>
createStrategy(SuspectGame<S> suspectGame, SuspectSolver.SuspectSolution<S> suspectSolution, AcceptingLasso<S> lasso) {
createStrategy(SuspectGame<S> suspectGame, SuspectSolver.HistorySolution<S> historySolution, AcceptingLasso<S> lasso) {
Iterator<RunGraph.RunState<S>> iterator = lasso.states(true).iterator();
var current = iterator.next();
assert current.historyState().equals(suspectGame.initialState().historyState());
......@@ -35,10 +34,9 @@ public final class StrategyMapper {
.iterator().next();
runGraphMoves.put(current, move);
EveState<S> eveState = new EveState<>(current.historyState(), agents);
assert suspectSolution.isWinning(eveState);
assert historySolution.isWinning(current.historyState());
// For each deviation, provide a proof that we can punish someone
punishmentStrategy.put(current, suspectSolution.strategy(eveState));
punishmentStrategy.put(current, historySolution.strategy(current.historyState()));
current = next;
}
return new EquilibriumStrategy<>(lasso, Map.copyOf(runGraphMoves), Map.copyOf(punishmentStrategy));
......
......@@ -2,16 +2,17 @@ package com.cges.algorithm;
import static com.google.common.base.Preconditions.checkArgument;
import com.cges.algorithm.HistoryGame.HistoryState;
import com.cges.algorithm.SuspectGame.EveState;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.PayoffAssignment;
import com.cges.parity.Player;
import com.cges.parity.SuspectParityGame;
import com.cges.model.Transition;
import com.cges.parity.OinkGameSolver;
import com.cges.parity.Player;
import com.cges.parity.PriorityState;
import com.cges.parity.SuspectParityGame;
import java.util.ArrayDeque;
import java.util.Collection;
import java.util.Comparator;
import java.util.Deque;
import java.util.HashMap;
import java.util.HashSet;
......@@ -20,6 +21,8 @@ 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 owl.automaton.Automaton;
import owl.automaton.MutableAutomatonUtil;
......@@ -28,8 +31,10 @@ import owl.automaton.acceptance.ParityAcceptance;
import owl.automaton.acceptance.optimization.AcceptanceOptimizations;
import owl.ltl.BooleanConstant;
import owl.ltl.Conjunction;
import owl.ltl.Formula;
import owl.ltl.Disjunction;
import owl.ltl.GOperator;
import owl.ltl.LabelledFormula;
import owl.ltl.Literal;
import owl.ltl.rewriter.LiteralMapper;
import owl.ltl.rewriter.SimplifierFactory;
import owl.run.Environment;
......@@ -37,7 +42,7 @@ import owl.translations.ltl2dpa.LTL2DPAFunction;
public final class SuspectSolver<S> {
private final Environment env = Environment.standard();
private final LTL2DPAFunction dpaFunction = new LTL2DPAFunction(env, LTL2DPAFunction.RECOMMENDED_SYMMETRIC_CONFIG);
private final LTL2DPAFunction dpaFunction = new LTL2DPAFunction(env, LTL2DPAFunction.RECOMMENDED_ASYMMETRIC_CONFIG);
private final SuspectGame<S> suspectGame;
// TODO Make caching work on unlabelled formulas?
private final Map<LabelledFormula, Automaton<Object, ParityAcceptance>> automatonCache = new HashMap<>();
......@@ -47,93 +52,29 @@ public final class SuspectSolver<S> {
this.suspectGame = suspectGame;
}
public interface SuspectSolution<S> {
Set<EveState<S>> winningStates();
default boolean isWinning(EveState<S> state) {
return winningStates().contains(state);
}
PriorityState<S> initial(EveState<S> state);
SuspectStrategy<S> strategy(EveState<S> state);
}
public interface SuspectStrategy<S> {
PriorityState<S> winningMove(PriorityState<S> state);
}
record Solution<S>(Map<EveState<S>, Strategy<S>> strategies) implements SuspectSolution<S> {
@Override
public Set<EveState<S>> winningStates() {
return strategies.keySet();
}
@Override
public PriorityState<S> initial(EveState<S> state) {
return strategies.get(state).initialState();
}
@Override
public SuspectStrategy<S> strategy(EveState<S> state) {
return strategies.get(state);
}
}
record Strategy<S>(PriorityState<S> initialState, Map<PriorityState<S>, PriorityState<S>> strategies) implements SuspectStrategy<S> {
@Override
public PriorityState<S> winningMove(PriorityState<S> state) {
checkArgument(strategies.containsKey(state));
return strategies.get(state);
}
}
public static <S> SuspectSolution<S> computeWinningEveStatesLimitSet(SuspectGame<S> suspectGame, PayoffAssignment payoff) {
// TODO Reuse winning / losing states
/*
SuccessorFunction<EveState<S>> successorFunction = current -> suspectGame.successors(current).stream()
.map(suspectGame::successors)
.flatMap(Collection::stream)
.collect(Collectors.toSet());
List<Set<EveState<S>>> decomposition = Lists.reverse(SccDecomposition.of(Set.of(suspectGame.initialState()), successorFunction).sccs());
assert decomposition.stream().flatMap(Collection::stream).collect(Collectors.toSet()).equals(suspectGame.eveStates());
*/
public static <S> HistorySolution<S> computeReachableWinningStates(SuspectGame<S> suspectGame, PayoffAssignment payoff) {
SuspectSolver<S> solver = new SuspectSolver<>(suspectGame);
Map<EveState<S>, Strategy<S>> strategies = new HashMap<>();
for (EveState<S> state : suspectGame.eveStates()) {
findEventualSuspects(suspectGame, state).stream()
.map(agents -> Conjunction.of(agents.stream()
.filter(payoff::isLoser)
.map(state.historyState()::goal)
.map(Formula::not)))
.sorted(Comparator.comparingInt(Formula::height)) // Try to solve "easy" formulae first
.map(formula -> LabelledFormula.of(formula, suspectGame.historyGame().concurrentGame().atomicPropositions()))
.flatMap(formula -> solver.isWinning(suspectGame, state, formula).stream())
.findFirst()
.ifPresent(strategy -> strategies.put(state, strategy));
}
return new Solution<>(Map.copyOf(strategies));
}
public static <S> SuspectSolution<S> computeReachableWinningEveStates(SuspectGame<S> suspectGame, PayoffAssignment payoff) {
SuspectSolver<S> solver = new SuspectSolver<>(suspectGame);
Map<EveState<S>, Strategy<S>> strategies = new HashMap<>();
List<String> atomicPropositions = suspectGame.historyGame().concurrentGame().atomicPropositions();
Set<EveState<S>> states = new HashSet<>(List.of(suspectGame.initialState()));
Queue<EveState<S>> queue = new ArrayDeque<>(states);
Map<HistoryState<S>, Strategy<S>> strategies = new HashMap<>();
HistoryGame<S> historyGame = suspectGame.historyGame();
ConcurrentGame<S> concurrentGame = historyGame.concurrentGame();
Set<Agent> losingAgents = concurrentGame.agents().stream().filter(payoff::isLoser).collect(Collectors.toSet());
List<String> atomicPropositions = Stream.concat(
concurrentGame.atomicPropositions().stream(),
losingAgents.stream().map(Agent::name)).toList();
Map<Agent, Literal> agentLiterals = losingAgents.stream().collect(Collectors.toMap(Function.identity(),
a -> Literal.of(atomicPropositions.indexOf(a.name()))));
assert Set.copyOf(atomicPropositions).size() == atomicPropositions.size();
Set<HistoryState<S>> states = new HashSet<>(List.of(historyGame.initialState()));
Queue<HistoryState<S>> queue = new ArrayDeque<>(states);
while (!queue.isEmpty()) {
EveState<S> state = queue.poll();
solver.isWinning(suspectGame, state, LabelledFormula.of(Conjunction.of(state.suspects().stream()
.filter(payoff::isLoser)
.map(state.historyState()::goal)
.map(Formula::not)),
atomicPropositions)).ifPresent(strategy -> {
HistoryState<S> state = queue.poll();
LabelledFormula formula = LabelledFormula.of(Disjunction.of(
losingAgents.stream().map(a -> Conjunction.of(GOperator.of(agentLiterals.get(a)), state.goal(a)))), atomicPropositions);
solver.isWinning(suspectGame, new EveState<>(state, concurrentGame.agents()), formula.not()).ifPresent(strategy -> {
strategies.put(state, strategy);
suspectGame.successors(state).stream().map(suspectGame::successors).flatMap(Collection::stream).forEach(successor -> {
historyGame.transitions(state).map(Transition::destination).forEach(successor -> {
if (states.add(successor)) {
queue.add(successor);
}
......@@ -143,8 +84,8 @@ public final class SuspectSolver<S> {
return new Solution<>(Map.copyOf(strategies));
}
private Optional<Strategy<S>> isWinning(SuspectGame<S> game, EveState<S> eveState, LabelledFormula agentGoal) {
var goal = SimplifierFactory.apply(agentGoal, SimplifierFactory.Mode.SYNTACTIC_FIXPOINT);
private Optional<Strategy<S>> isWinning(SuspectGame<S> game, EveState<S> eveState, LabelledFormula eveGoal) {
var goal = SimplifierFactory.apply(eveGoal, SimplifierFactory.Mode.SYNTACTIC_FIXPOINT);
if (goal.formula() instanceof BooleanConstant bool) {
if (bool.value) {
PriorityState<S> state = new PriorityState<>(null, eveState, 0);
......@@ -227,4 +168,45 @@ public final class SuspectSolver<S> {
}
return potentialLimitSuspectAgents;
}
public interface HistorySolution<S> {
Set<HistoryState<S>> winningStates();
default boolean isWinning(HistoryState<S> state) {
return winningStates().contains(state);
}
PriorityState<S> initial(HistoryState<S> state);
SuspectStrategy<S> strategy(HistoryState<S> state);
}
public interface SuspectStrategy<S> {
PriorityState<S> winningMove(PriorityState<S> state);
}
record Solution<S>(Map<HistoryState<S>, Strategy<S>> strategies) implements HistorySolution<S> {
@Override
public Set<HistoryState<S>> winningStates() {
return strategies.keySet();
}
@Override
public PriorityState<S> initial(HistoryState<S> state) {
return strategies.get(state).initialState();
}
@Override
public SuspectStrategy<S> strategy(HistoryState<S> state) {
return strategies.get(state);
}
}
record Strategy<S>(PriorityState<S> initialState, Map<PriorityState<S>, PriorityState<S>> strategies) implements SuspectStrategy<S> {
@Override
public PriorityState<S> winningMove(PriorityState<S> state) {
checkArgument(strategies.containsKey(state));
return strategies.get(state);
}
}
}
......@@ -4,8 +4,10 @@ import static com.google.common.base.Preconditions.checkArgument;
import com.cges.algorithm.SuspectGame;
import com.cges.algorithm.SuspectGame.EveState;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.google.common.collect.Iterables;
import de.tum.in.naturals.bitset.BitSets;
import java.util.BitSet;
import java.util.Collection;
import java.util.List;
......@@ -25,6 +27,7 @@ public final class SuspectParityGame<S> implements ParityGame<PriorityState<S>>
private final Automaton<Object, ParityAcceptance> dpa;
private final Map<S, BitSet> labelCache;
private final int maximumPriority;
private final Map<String, Integer> propositionIndex;
private SuspectParityGame(SuspectGame<S> suspectGame, PriorityState<S> initialState, Automaton<Object, ParityAcceptance> dpa) {
assert !dpa.acceptance().parity().max();
......@@ -41,7 +44,7 @@ public final class SuspectParityGame<S> implements ParityGame<PriorityState<S>>
this.maximumPriority = maximumPriority;
List<String> propositions = dpa.factory().atomicPropositions();
Map<String, Integer> propositionIndex = IntStream.range(0, propositions.size())
propositionIndex = IntStream.range(0, propositions.size())
.boxed()
.collect(Collectors.toMap(propositions::get, Function.identity()));
ConcurrentGame<S> concurrentGame = suspectGame.historyGame().concurrentGame();
......@@ -66,7 +69,9 @@ public final class SuspectParityGame<S> implements ParityGame<PriorityState<S>>
@Override
public Stream<PriorityState<S>> successors(PriorityState<S> current) {
if (current.isEve()) {
BitSet label = labelCache.get(current.eve().gameState());
BitSet label = BitSets.copyOf(labelCache.get(current.eve().gameState()));
current.eve().suspects().stream().map(Agent::name).map(propositionIndex::get).filter(Objects::nonNull).forEach(label::set);
assert dpa.edges(current.automatonState(), label).size() == 1;
Edge<Object> automatonEdge = dpa.edge(current.automatonState(), label);
assert automatonEdge != null;
......
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