Commit 71a35068 authored by Tobias MEGGENDORFER's avatar Tobias MEGGENDORFER
Browse files

Snap

parent 37b2a91c
{
"name": "test1",
"type": "explicit",
"expected": [
{
"A1": false
}
],
"ap": [
"s1"
],
"agents": {
"A1": {
"goal": "G s1",
"payoff": "?",
"actions": [
"a"
]
}
},
"arena": {
"initial": "s0",
"states": {
"s0": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a"
},
"to": "s1"
}
]
},
"s1": {
"labels": [
"s1"
],
"transitions": [
{
"actions": {
"A1": "a"
},
"to": "s1"
}
]
}
}
}
}
\ No newline at end of file
{
"name": "test2",
"type": "explicit",
"expected": [
{
"A1": true,
"A2": false
}
],
"ap": [
"s1"
],
"agents": {
"A1": {
"goal": "F s1",
"payoff": "?",
"actions": [
"a"
]
},
"A2": {
"goal": "G !s1",
"payoff": "?",
"actions": [
"a"
]
}
},
"arena": {
"initial": "s0",
"states": {
"s0": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a"
},
"to": "s1"
}
]
},
"s1": {
"labels": [
"s1"
],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a"
},
"to": "s2"
}
]
},
"s2": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a"
},
"to": "s2"
}
]
}
}
}
}
\ No newline at end of file
{
"name": "test3",
"type": "explicit",
"expected": [
{
"A1": true,
"A2": false
},
{
"A1": true,
"A2": true
}
],
"ap": [
"a1", "a2", "b1", "b2"
],
"agents": {
"A1": {
"goal": "true",
"payoff": "?",
"actions": [
"a", "b"
]
},
"A2": {
"goal": "G ((a1 -> X X a2) & (b1 -> X X b2))",
"payoff": "?",
"actions": [
"a", "b"
]
}
},
"arena": {
"initial": "s0",
"states": {
"s0": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "*",
"A2": "a"
},
"to": "a1"
},
{
"actions": {
"A1": "*",
"A2": "b"
},
"to": "b1"
}
]
},
"a1": {
"labels": [
"a1"
],
"transitions": [
{
"actions": {
"A1": "*",
"A2": "*"
},
"to": "s1"
}
]
},
"b1": {
"labels": [
"b1"
],
"transitions": [
{
"actions": {
"A1": "*",
"A2": "*"
},
"to": "s1"
}
]
},
"s1": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "*"
},
"to": "a2"
},
{
"actions": {
"A1": "b",
"A2": "*"
},
"to": "b2"
}
]
},
"a2": {
"labels": [
"a2"
],
"transitions": [
{
"actions": {
"A1": "*",
"A2": "*"
},
"to": "a2"
}
]
},
"b2": {
"labels": [
"b2"
],
"transitions": [
{
"actions": {
"A1": "*",
"A2": "*"
},
"to": "b2"
}
]
}
}
}
}
\ No newline at end of file
package com.cges;
import com.cges.algorithm.FormulaHistoryGame;
import com.cges.algorithm.RunGraph;
import com.cges.algorithm.RunGraphSccSolver;
import com.cges.algorithm.SuspectGame;
import static com.google.common.base.Preconditions.checkArgument;
import com.cges.algorithm.RunGraphSolver;
import com.cges.graph.FormulaHistoryGame;
import com.cges.graph.RunGraph;
import com.cges.graph.SuspectGame;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.EquilibriumStrategy;
......@@ -12,16 +14,24 @@ import com.cges.output.Formatter;
import com.cges.parser.GameParser;
import com.google.common.base.Stopwatch;
import com.google.common.collect.Sets;
import com.google.gson.JsonArray;
import com.google.gson.JsonElement;
import com.google.gson.JsonObject;
import com.google.gson.JsonParser;
import java.io.BufferedReader;
import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Path;
import java.util.Comparator;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import javax.annotation.Nullable;
public final class Main {
private Main() {}
......@@ -29,13 +39,33 @@ public final class Main {
public static void main(String[] args) throws IOException {
Stopwatch overall = Stopwatch.createStarted();
ConcurrentGame<?> game;
@Nullable
Set<Map<Agent, Boolean>> validationSet;
if ("game".equals(args[0])) {
try (BufferedReader reader = Files.newBufferedReader(Path.of(args[1]))) {
game = GameParser.parseExplicit(reader.lines());
}
validationSet = null;
} else {
try (BufferedReader reader = Files.newBufferedReader(Path.of(args[0]))) {
game = GameParser.parseExplicit(JsonParser.parseReader(reader).getAsJsonObject());
JsonObject jsonObject = JsonParser.parseReader(reader).getAsJsonObject();
game = GameParser.parseExplicit(jsonObject);
JsonArray validation = jsonObject.getAsJsonArray("expected");
if (validation == null) {
validationSet = null;
} else {
validationSet = new HashSet<>();
for (JsonElement jsonElement : validation) {
Map<Agent, Boolean> expectedResult = new HashMap<>();
for (Map.Entry<String, JsonElement> entry : jsonElement.getAsJsonObject().entrySet()) {
Agent agent = game.agent(entry.getKey());
boolean payoff = entry.getValue().getAsBoolean();
expectedResult.put(agent, payoff);
}
checkArgument(expectedResult.keySet().equals(game.agents()), "Invalid valdation specification");
validationSet.add(expectedResult);
}
}
}
}
var list = analyse(game).peek(solution -> System.out.printf("Found NE for %s:%n%s%n",
......@@ -44,6 +74,23 @@ public final class Main {
System.out.println("Overall: " + overall);
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);
if (validationSet != null) {
Set<Map<Agent, Boolean>> results = list.stream().map(GameSolution::assignment)
.map(p -> game.agents().stream().collect(Collectors.toUnmodifiableMap(Function.identity(), p::isWinner)))
.collect(Collectors.toUnmodifiableSet());
if (!results.equals(validationSet)) {
var agents = game.agents().stream().sorted(Comparator.comparing(Agent::name)).toList();
System.out.println("Expected equilibrium:");
for (Map<Agent, Boolean> map : validationSet) {
System.out.println(agents.stream().map(a -> "%s:%s".formatted(a.name(), map.get(a))).collect(Collectors.joining(",", "[", "]")));
}
System.out.println("Found equilibrium:");
for (Map<Agent, Boolean> map : results) {
System.out.println(agents.stream().map(a -> "%s:%s".formatted(a.name(), map.get(a))).collect(Collectors.joining(",", "[", "]")));
}
System.exit(1);
}
}
}
private static <S> Stream<GameSolution<S>> analyse(ConcurrentGame<S> game) {
......@@ -54,11 +101,11 @@ public final class Main {
.collect(Collectors.toSet());
return Sets.powerSet(undefinedAgents).stream()
.map(PayoffAssignment::new)
.peek(p -> System.out.printf("Processing: %s%n", Formatter.format(p, game)))
.map(payoff -> {
Stopwatch solutionStopwatch = Stopwatch.createStarted();
var strategy = RunGraphSccSolver.solve(new RunGraph<>(suspectGame, payoff));
System.out.println("Solution: " + solutionStopwatch);
System.out.printf("Processing: %s%n", Formatter.format(payoff, game));
Stopwatch timer = Stopwatch.createStarted();
var strategy = RunGraphSolver.solve(new RunGraph<S>(suspectGame, payoff));
System.out.println("Solution: " + timer);
return strategy.map(s -> new GameSolution<>(payoff, s));
}).flatMap(Optional::stream);
}
......
......@@ -2,8 +2,10 @@ 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.graph.HistoryGame;
import com.cges.graph.HistoryGame.HistoryState;
import com.cges.graph.SuspectGame;
import com.cges.graph.SuspectGame.EveState;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.PayoffAssignment;
......@@ -21,7 +23,6 @@ import java.util.Optional;
import java.util.Queue;
import java.util.Set;
import java.util.function.Function;
import java.util.function.Supplier;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import owl.automaton.Automaton;
......@@ -41,13 +42,18 @@ import owl.translations.LtlTranslationRepository.Option;
public final class DeviationSolver<S> {
private static final boolean CROSS_VALIDATE = false;
private final Function<LabelledFormula, Automaton<?, ? extends ParityAcceptance>> dpaFunction =
/* LtlTranslationRepository.defaultTranslation(EnumSet.of(Option.COMPLETE, Option.SIMPLIFY_AUTOMATON),
BranchingMode.DETERMINISTIC, ParityAcceptance.class); */
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;
// TODO Make caching work on unlabelled formulas?
private final Map<LabelledFormula, Automaton<?, ?>> automatonCache = new HashMap<>();
private final OinkGameSolver solver = new OinkGameSolver();
private final Map<Agent, Literal> agentLiterals;
......@@ -55,6 +61,11 @@ public final class DeviationSolver<S> {
private final Set<Agent> losingAgents;
private final Map<HistoryState<S>, PunishmentStrategy<S>> cache = new HashMap<>();
@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));
public DeviationSolver(SuspectGame<S> suspectGame, PayoffAssignment payoff) {
this.suspectGame = suspectGame;
......@@ -65,13 +76,24 @@ public final class DeviationSolver<S> {
agentLiterals = losingAgents.stream().collect(Collectors.toMap(Function.identity(),
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
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)) {
return Optional.ofNullable(cache.get(historyState));
PunishmentStrategy<S> strategy = cache.get(historyState);
assert doSolve(historyState).isPresent() == (strategy != null);
return Optional.ofNullable(strategy);
}
return doSolve(historyState);
}
private Optional<PunishmentStrategy<S>> doSolve(HistoryState<S> historyState) {
LabelledFormula eveGoal = LabelledFormula.of(Disjunction.of(losingAgents.stream()
.map(a -> Conjunction.of(GOperator.of(agentLiterals.get(a)), historyState.goal(a)))).not(), atomicPropositions);
......@@ -81,37 +103,29 @@ public final class DeviationSolver<S> {
if (goal.formula() instanceof BooleanConstant bool) {
if (bool.value) {
PriorityState<S> state = new PriorityState<>(null, eveState, 0);
return Optional.of(new Strategy<>(state, Map.of(state, state)));
Strategy<S> strategy = new Strategy<>(state, Map.of(state, state));
cache.put(historyState, strategy);
return Optional.of(strategy);
}
cache.put(historyState, null);
return Optional.empty();
}
var shifted = LiteralMapper.shiftLiterals(goal);
@SuppressWarnings("unchecked")
var automaton = (Automaton<Object, ParityAcceptance>) automatonCache.computeIfAbsent(shifted.formula,
formula -> ParityUtil.convert(dpaFunction.apply(formula), ParityAcceptance.Parity.MIN_EVEN));
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);
assert !CROSS_VALIDATE || paritySolution.winner(parityGame.initialState()).equals(((Supplier<Player>) () -> {
var defaultTranslation = LtlTranslationRepository.LtlToDpaTranslation.DEFAULT.translation(EnumSet.of(Option.COMPLETE));
@SuppressWarnings("unchecked")
var otherGame = SuspectParityGame.create(suspectGame, eveState, (Automaton<Object, ParityAcceptance>)
ParityUtil.convert(defaultTranslation.apply(shifted.formula), ParityAcceptance.Parity.MIN_EVEN));
var otherSolution = solver.solve(otherGame);
return otherSolution.winner(otherGame.initialState());
}).get());
if (paritySolution.winner(parityGame.initialState()) == Player.EVEN) {
return Optional.empty();
}
Queue<PriorityState<S>> queue = new ArrayDeque<>(List.of(parityGame.initialState()));
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()) {
......@@ -131,19 +145,22 @@ public final class DeviationSolver<S> {
}
});
}
var strategyCopy = Map.copyOf(strategy);
for (PriorityState<S> priorityState : reached) {
if (priorityState.isEve() && priorityState.eve().suspects().equals(losingAgents)) {
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);
}
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);
}
}
if (paritySolution.winner(parityGame.initialState()) == Player.EVEN) {
return Optional.empty();
}
return Optional.of(new Strategy<>(parityGame.initialState(), strategyCopy));
}
......
......@@ -3,7 +3,10 @@ package com.cges.algorithm;
import static com.google.common.base.Preconditions.checkNotNull;
import static com.google.common.base.Preconditions.checkState;
import com.cges.algorithm.RunGraph.RunState;
import com.cges.graph.RunGraph;
import com.cges.graph.RunGraph.RunState;
import com.google.common.collect.HashMultimap;
import com.google.common.collect.SetMultimap;
import com.microsoft.z3.BitVecExpr;
import com.microsoft.z3.BitVecNum;
import com.microsoft.z3.BitVecSort;
......@@ -18,142 +21,192 @@ import com.microsoft.z3.Z3Exception;
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Comparator;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
import java.util.PriorityQueue;
import java.util.Queue;
import java.util.Set;
import java.util.logging.Level;
import java.util.logging.Logger;
import java.util.stream.IntStream;
public final class RunGraphBmcSolver {
public final class RunGraphBmcSolver<S> {
private static final Logger logger = Logger.getLogger(RunGraphBmcSolver.class.getName());
private RunGraphBmcSolver() {}
private final RunGraph<S> graph;
private final Set<RunState<S>> explored;
private final List<RunState<S>> stateNumbering = new ArrayList<>();
@SuppressWarnings("unchecked")
public static <S> List<RunState<S>> check(RunGraph<S> graph) {
// TODO Derive upper bound on depth from graph
// TODO QBF or similar instead of bit encoding
private final Context ctx;
private final Queue<Distance<S>> queue;
private int exploredDepth = 0;
private final SetMultimap<RunState<S>, RunState<S>> acceptingTransitions = HashMultimap.create();
Set<RunState<S>> states = new HashSet<>(graph.initialStates());
Queue<RunState<S>> queue = new ArrayDeque<>(states);
while (!queue.isEmpty()) {
var state = queue.poll();
graph.successors(state).forEach(successor -> {
if (states.add(successor)) {
queue.add(successor);
}
});
}
private record Distance<S>(RunState<S> state, int distance) {}
// TODO