Commit 37b2a91c authored by Tobias MEGGENDORFER's avatar Tobias MEGGENDORFER
Browse files

Fix

parent 15f4d0b4
......@@ -35,7 +35,7 @@ repositories {
dependencies {
// Owl
implementation(files("lib/owl-20.06.jar", "lib/jhoafparser-1.1.1-patched.jar"))
implementation(files("lib/owl-21.0.jar", "lib/jhoafparser-1.1.1-patched.jar"))
implementation("de.tum.in", "jbdd", "0.5.2")
implementation("de.tum.in", "naturals-util", "0.16.0")
implementation("commons-cli", "commons-cli", "1.4")
......@@ -62,7 +62,6 @@ configurations {
application {
mainClass.set("com.cges.Main")
applicationDefaultJvmArgs = listOf("-ea")
}
tasks.generateGrammarSource {
......
......@@ -6,6 +6,7 @@ if __name__ == "__main__":
json.dump({
"name": f"gossip{n}",
"ap": [f"g{i}" for i in range(1, n + 1)],
"type": "module",
"modules": {
f"A{i}": {
"goal": f"G F g{i}",
......
{
"name": "gossip2",
"ap": [
"g1",
"g2"
],
"agents": {
"A1": {
"goal": "G F g1",
"payoff": true,
"actions": [
"a",
"g",
"w"
]
},
"A2": {
"goal": "G F g2",
"payoff": true,
"actions": [
"a",
"g",
"w"
]
}
},
"arena": {
"initial": "s0",
"states": {
"s0": {
"labels": [],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a"
},
"to": "s0"
},
{
"actions": {
"A1": "a",
"A2": "g"
},
"to": "s1"
},
{
"actions": {
"A1": "g",
"A2": "a"
},
"to": "s2"
},
{
"actions": {
"A1": "g",
"A2": "g"
},
"to": "s3"
}
]
},
"s1": {
"labels": [
"g2"
],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "w"
},
"to": "s1"
},
{
"actions": {
"A1": "g",
"A2": "w"
},
"to": "s3"
}
]
},
"s2": {
"labels": [
"g1"
],
"transitions": [
{
"actions": {
"A1": "w",
"A2": "a"
},
"to": "s2"
},
{
"actions": {
"A1": "w",
"A2": "g"
},
"to": "s3"
}
]
},
"s3": {
"labels": [
"g1",
"g2"
],
"transitions": [
{
"actions": {
"A1": "a",
"A2": "a"
},
"to": "s0"
}
]
}
}
}
}
\ No newline at end of file
{
"name": "example",
"type": "explicit",
"ap": [
"s1",
"s2"
......
{
"name": "gossip2",
"type": "module",
"ap": [
"g1",
"g2"
......@@ -7,7 +8,7 @@
"modules": {
"A1": {
"goal": "G F g1",
"payoff": true,
"payoff": "?",
"actions": ["a", "g", "w"],
"labels": ["g1"],
"initial": "s11",
......@@ -46,7 +47,7 @@
},
"A2": {
"goal": "G F g2",
"payoff": true,
"payoff": "?",
"actions": ["a", "g", "w"],
"labels": ["g2"],
"initial": "s21",
......
{
"name": "gossip3",
"type": "module",
"ap": [
"g1",
"g2",
......
{
"name": "gossip4",
"type": "module",
"ap": [
"g1",
"g2",
......
{
"name": "gossip6",
"type": "module",
"ap": [
"g1",
"g2",
......
{
"name": "gossip8",
"type": "module",
"ap": [
"g1",
"g2",
......
......@@ -3,17 +3,13 @@ package com.cges;
import com.cges.algorithm.FormulaHistoryGame;
import com.cges.algorithm.RunGraph;
import com.cges.algorithm.RunGraphSccSolver;
import com.cges.algorithm.StrategyMapper;
import com.cges.algorithm.SuspectGame;
import com.cges.algorithm.SuspectSolver;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.EquilibriumStrategy;
import com.cges.model.PayoffAssignment;
import com.cges.output.Formatter;
import com.cges.parser.ExplicitParser;
import com.cges.parser.GameParser;
import com.cges.parser.ModuleParser;
import com.google.common.base.Stopwatch;
import com.google.common.collect.Sets;
import com.google.gson.JsonParser;
......@@ -21,6 +17,7 @@ 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.Optional;
import java.util.Set;
import java.util.stream.Collectors;
......@@ -32,35 +29,25 @@ public final class Main {
public static void main(String[] args) throws IOException {
Stopwatch overall = Stopwatch.createStarted();
ConcurrentGame<?> game;
switch (args[0]) {
case "game":
try (BufferedReader reader = Files.newBufferedReader(Path.of(args[1]))) {
game = GameParser.parse(reader.lines());
}
break;
case "explicit":
try (BufferedReader reader = Files.newBufferedReader(Path.of(args[1]))) {
game = ExplicitParser.parse(JsonParser.parseReader(reader).getAsJsonObject());
}
break;
case "module":
try (BufferedReader reader = Files.newBufferedReader(Path.of(args[1]))) {
game = ModuleParser.parse(JsonParser.parseReader(reader).getAsJsonObject());
}
break;
default:
throw new IllegalArgumentException(args[0]);
if ("game".equals(args[0])) {
try (BufferedReader reader = Files.newBufferedReader(Path.of(args[1]))) {
game = GameParser.parseExplicit(reader.lines());
}
} else {
try (BufferedReader reader = Files.newBufferedReader(Path.of(args[0]))) {
game = GameParser.parseExplicit(JsonParser.parseReader(reader).getAsJsonObject());
}
}
analyse(game).forEach(solution -> System.out.printf("Found NE for %s:%n%s%n",
var list = analyse(game).peek(solution -> System.out.printf("Found NE for %s:%n%s%n",
Formatter.format(solution.assignment(), game),
solution.strategy()));
solution.strategy())).collect(Collectors.toList());
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);
}
private static <S> Stream<GameSolution<S>> analyse(ConcurrentGame<S> game) {
Stopwatch suspectStopwatch = Stopwatch.createStarted();
var suspectGame = SuspectGame.create(new FormulaHistoryGame<>(game));
System.out.printf("Suspect: %s, %d states%n", suspectStopwatch, suspectGame.eveStates().size());
var suspectGame = new SuspectGame<>(new FormulaHistoryGame<>(game));
Set<Agent> undefinedAgents = game.agents().stream()
.filter(a -> a.payoff().equals(Agent.Payoff.UNDEFINED))
......@@ -68,21 +55,11 @@ public final class Main {
return Sets.powerSet(undefinedAgents).stream()
.map(PayoffAssignment::new)
.peek(p -> System.out.printf("Processing: %s%n", Formatter.format(p, game)))
.<Optional<GameSolution<S>>>map(payoff -> {
Stopwatch winningStopwatch = Stopwatch.createStarted();
var suspectSolution = SuspectSolver.computeReachableWinningStates(suspectGame, payoff);
System.out.println("Winning: " + winningStopwatch);
.map(payoff -> {
Stopwatch solutionStopwatch = Stopwatch.createStarted();
var runGraph = RunGraph.create(suspectGame.historyGame(), payoff, suspectSolution::isWinning);
var lasso = RunGraphSccSolver.solve(runGraph);
var strategy = RunGraphSccSolver.solve(new RunGraph<>(suspectGame, payoff));
System.out.println("Solution: " + solutionStopwatch);
if (lasso.isPresent()) {
var strategy = StrategyMapper.createStrategy(suspectGame, suspectSolution, lasso.get());
return Optional.of(new GameSolution<>(payoff, strategy));
} else {
return Optional.empty();
}
return strategy.map(s -> new GameSolution<>(payoff, s));
}).flatMap(Optional::stream);
}
......
......@@ -7,13 +7,12 @@ import com.cges.algorithm.SuspectGame.EveState;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.PayoffAssignment;
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.Deque;
import java.util.EnumSet;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
......@@ -22,13 +21,12 @@ 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;
import owl.automaton.MutableAutomatonUtil;
import owl.automaton.ParityUtil;
import owl.automaton.acceptance.ParityAcceptance;
import owl.automaton.acceptance.optimization.AcceptanceOptimizations;
import owl.ltl.BooleanConstant;
import owl.ltl.Conjunction;
import owl.ltl.Disjunction;
......@@ -36,56 +34,50 @@ 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;
import owl.translations.ltl2dpa.LTL2DPAFunction;
import owl.ltl.rewriter.SimplifierRepository;
import owl.translations.LtlTranslationRepository;
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); */
LtlTranslationRepository.LtlToDpaTranslation.SEJK16_EKRS17.translation(EnumSet.of(Option.SIMPLIFY_AUTOMATON));
public final class SuspectSolver<S> {
private final Environment env = Environment.standard();
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<>();
private final Map<LabelledFormula, Automaton<?, ?>> automatonCache = new HashMap<>();
private final OinkGameSolver solver = new OinkGameSolver();
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 SuspectSolver(SuspectGame<S> suspectGame) {
public DeviationSolver(SuspectGame<S> suspectGame, PayoffAssignment payoff) {
this.suspectGame = suspectGame;
}
public static <S> HistorySolution<S> computeReachableWinningStates(SuspectGame<S> suspectGame, PayoffAssignment payoff) {
SuspectSolver<S> solver = new SuspectSolver<>(suspectGame);
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(),
losingAgents = concurrentGame.agents().stream().filter(payoff::isLoser).collect(Collectors.toSet());
atomicPropositions = Stream.concat(concurrentGame.atomicPropositions().stream(), losingAgents.stream().map(Agent::name)).toList();
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()) {
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);
historyGame.transitions(state).map(Transition::destination).forEach(successor -> {
if (states.add(successor)) {
queue.add(successor);
}
});
});
public Optional<PunishmentStrategy<S>> solve(HistoryState<S> historyState) {
if (cache.containsKey(historyState)) {
return Optional.ofNullable(cache.get(historyState));
}
return new Solution<>(Map.copyOf(strategies));
}
private Optional<Strategy<S>> isWinning(SuspectGame<S> game, EveState<S> eveState, LabelledFormula eveGoal) {
var goal = SimplifierFactory.apply(eveGoal, SimplifierFactory.Mode.SYNTACTIC_FIXPOINT);
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);
......@@ -95,31 +87,26 @@ public final class SuspectSolver<S> {
}
var shifted = LiteralMapper.shiftLiterals(goal);
Automaton<Object, ParityAcceptance> automaton = automatonCache.computeIfAbsent(shifted.formula, formula -> {
@SuppressWarnings("unchecked")
Automaton<Object, ParityAcceptance> dpa = (Automaton<Object, ParityAcceptance>) dpaFunction.apply(formula);
MutableAutomatonUtil.Sink sink = new MutableAutomatonUtil.Sink();
var mutable = MutableAutomatonUtil.asMutable(
ParityUtil.convert(dpa, ParityAcceptance.Parity.MIN_EVEN, sink));
var minimized = AcceptanceOptimizations.optimize(mutable);
minimized.trim();
if (minimized.size() == 0) {
return minimized;
}
if (minimized.acceptance().acceptanceSets() == 1) {
// Hack needed for .complete to work
minimized.acceptance(minimized.acceptance().withAcceptanceSets(2));
}
MutableAutomatonUtil.complete(minimized, sink);
return minimized;
});
if (automaton.size() == 0) {
@SuppressWarnings("unchecked")
var automaton = (Automaton<Object, ParityAcceptance>) automatonCache.computeIfAbsent(shifted.formula,
formula -> ParityUtil.convert(dpaFunction.apply(formula), ParityAcceptance.Parity.MIN_EVEN));
if (automaton.states().isEmpty()) {
return Optional.empty();
}
var parityGame = SuspectParityGame.create(game, eveState, automaton);
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();
}
......@@ -144,67 +131,31 @@ public final class SuspectSolver<S> {
}
});
}
return Optional.of(new Strategy<>(parityGame.initialState(), Map.copyOf(strategy)));
}
public static <S> Set<Set<Agent>> findEventualSuspects(SuspectGame<S> game, EveState<S> root) {
Deque<EveState<S>> queue = new ArrayDeque<>(List.of(root));
Set<EveState<S>> states = new HashSet<>(queue);
Set<Set<Agent>> potentialLimitSuspectAgents = new HashSet<>();
while (!queue.isEmpty()) {
EveState<S> current = queue.pollLast();
for (SuspectGame.AdamState<S> adamSuccessor : game.successors(current)) {
assert adamSuccessor.eveState().equals(current);
for (EveState<S> eveSuccessor : game.successors(adamSuccessor)) {
assert current.suspects().containsAll(eveSuccessor.suspects());
if (states.add(eveSuccessor)) {
queue.addLast(eveSuccessor);
} else {
potentialLimitSuspectAgents.add(eveSuccessor.suspects());
}
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);
}
}
}
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);
return Optional.of(new Strategy<>(parityGame.initialState(), strategyCopy));
}
record Solution<S>(Map<HistoryState<S>, Strategy<S>> strategies) implements HistorySolution<S> {
@Override
public Set<HistoryState<S>> winningStates() {
return strategies.keySet();
}
public interface PunishmentStrategy<S> {
PriorityState<S> initialState();
@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);
}
PriorityState<S> move(PriorityState<S> state);
}
record Strategy<S>(PriorityState<S> initialState, Map<PriorityState<S>, PriorityState<S>> strategies) implements SuspectStrategy<S> {
record Strategy<S>(PriorityState<S> initialState, Map<PriorityState<S>, PriorityState<S>> strategies) implements PunishmentStrategy<S> {
@Override
public PriorityState<S> winningMove(PriorityState<S> state) {
public PriorityState<S> move(PriorityState<S> state) {
checkArgument(strategies.containsKey(state));
return strategies.get(state);
}
......
......@@ -4,6 +4,7 @@ import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.Transition;
import com.google.common.collect.ImmutableSetMultimap;
import com.google.common.collect.Lists;
import com.google.common.collect.SetMultimap;
import de.tum.in.naturals.Indices;
import java.util.ArrayDeque;
......@@ -19,21 +20,18 @@ import java.util.Queue;
import java.util.Set;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import owl.factories.EquivalenceClassFactory;
import owl.factories.jbdd.JBddSupplier;
import owl.ltl.EquivalenceClass;
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 static final Formula[] EMPTY = new Formula[0];
private final S state;
private final EquivalenceClass[] agentGoals;
private final Formula[] agentGoals;
private final Map<Agent, Integer> agentIndices;
private final int hashCode;
ListHistoryState(S state, List<EquivalenceClass> agentGoals, Map<Agent, Integer> agentIndices) {
ListHistoryState(S state, List<Formula> agentGoals, Map<Agent, Integer> agentIndices) {
this.state = state;
this.agentGoals = agentGoals.toArray(EMPTY);