Commit 952af6d0 authored by Tobias MEGGENDORFER's avatar Tobias MEGGENDORFER
Browse files

Small formatting improvements

parent b238baa6
package com.cges;
import com.cges.graph.RunGraph;
import com.cges.graph.SuspectGame;
import com.cges.model.EquilibriumStrategy;
import com.cges.model.PayoffAssignment;
public record GameSolution<S>(SuspectGame<S> suspectGame, RunGraph<S> runGraph, PayoffAssignment assignment,
EquilibriumStrategy<S> strategy) {}
......@@ -8,7 +8,6 @@ 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;
import com.cges.model.PayoffAssignment;
import com.cges.output.DotWriter;
import com.cges.output.Formatter;
......@@ -81,6 +80,9 @@ public final class Main {
Formatter.format(solution.assignment(), game),
solution.strategy())).collect(Collectors.toList());
System.out.println("Overall: " + overall);
for (GameSolution<?> gameSolution : list) {
DotWriter.writeSolution(gameSolution, System.out);
}
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) {
......@@ -113,11 +115,11 @@ public final class Main {
.map(payoff -> {
System.out.printf("Processing: %s%n", Formatter.format(payoff, game));
Stopwatch timer = Stopwatch.createStarted();
var strategy = RunGraphSolver.solve(new RunGraph<S>(suspectGame, payoff));
RunGraph<S> runGraph = new RunGraph<>(suspectGame, payoff);
var strategy = RunGraphSolver.solve(runGraph);
System.out.println("Solution: " + timer);
return strategy.map(s -> new GameSolution<>(payoff, s));
return strategy.map(s -> new GameSolution<>(suspectGame, runGraph, payoff, s));
}).flatMap(Optional::stream);
}
record GameSolution<S>(PayoffAssignment assignment, EquilibriumStrategy<S> strategy) {}
}
......@@ -58,7 +58,7 @@ public final class RunGraphSolver {
});
}
var path = RunGraphBmcSolver.search(graph);
var path = RunGraphSccSolver.search(graph);
if (path.isEmpty()) {
return Optional.empty();
}
......
......@@ -22,24 +22,32 @@ import owl.ltl.Formula;
import owl.ltl.rewriter.SimplifierRepository;
public class FormulaHistoryGame<S> implements HistoryGame<S> {
private final Map<Agent, Integer> indices;
static final class ListHistoryState<S> implements HistoryState<S> {
private static final Formula[] EMPTY = new Formula[0];
private final S state;
private final Formula[] agentGoals;
private final Map<Agent, Integer> agentIndices;
private final FormulaHistoryGame<S> game;
private final int hashCode;
ListHistoryState(S state, List<Formula> agentGoals, Map<Agent, Integer> agentIndices) {
ListHistoryState(S state, List<Formula> agentGoals, FormulaHistoryGame<S> game) {
this.state = state;
this.agentGoals = agentGoals.toArray(EMPTY);
this.agentIndices = Map.copyOf(agentIndices);
this.game = game;
this.hashCode = this.state.hashCode() ^ Arrays.hashCode(this.agentGoals);
}
@Override
public Formula goal(Agent agent) {
return agentGoals[agentIndices.get(agent)];
return agentGoals[game.indices.get(agent)];
}
@Override
public HistoryGame<S> game() {
return game;
}
@Override
......@@ -47,7 +55,7 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
return state;
}
public List<Formula> agentGoals() {
public List<Formula> goals() {
return Arrays.asList(agentGoals);
}
......@@ -67,7 +75,7 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
@Override
public String toString() {
return state + " " + agentIndices.entrySet().stream().sorted(Map.Entry.comparingByKey(Comparator.comparing(Agent::name)))
return state + " " + game.indices.entrySet().stream().sorted(Map.Entry.comparingByKey(Comparator.comparing(Agent::name)))
.map(Map.Entry::getValue)
.map(i -> agentGoals[i])
.map(SimplifierRepository.SYNTACTIC_FIXPOINT::apply)
......@@ -87,10 +95,10 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
Indices.forEachIndexed(game.atomicPropositions(), (index, proposition) -> propositionIndices.put(proposition, index));
Map<Agent, Integer> agentIndices = new HashMap<>();
Indices.forEachIndexed(game.agents(), (index, agent) -> agentIndices.put(agent, index));
Map<Agent, Integer> indices = Map.copyOf(agentIndices);
indices = Map.copyOf(agentIndices);
this.initialState = new ListHistoryState<>(game.initialState(),
game.agents().stream().map(Agent::goal).map(Formula::unfold).toList(), indices);
game.agents().stream().map(Agent::goal).map(Formula::unfold).toList(), this);
Map<HistoryState<S>, Set<Transition<HistoryState<S>>>> transitions = new HashMap<>();
Set<ListHistoryState<S>> states = new HashSet<>(List.of(initialState));
......@@ -104,10 +112,10 @@ public class FormulaHistoryGame<S> implements HistoryGame<S> {
game.labels(s).stream().map(propositionIndices::get).forEach(set::set);
return set;
});
List<Formula> successorGoals = List.copyOf(Lists.transform(state.agentGoals(), goal -> goal.temporalStep(valuation).unfold()));
List<Formula> successorGoals = List.copyOf(Lists.transform(state.goals(), goal -> goal.temporalStep(valuation).unfold()));
Set<Transition<HistoryState<S>>> stateTransitions = new HashSet<>();
for (Transition<S> transition : game.transitions(state.state())) {
ListHistoryState<S> successor = new ListHistoryState<>(transition.destination(), successorGoals, indices);
ListHistoryState<S> successor = new ListHistoryState<>(transition.destination(), successorGoals, this);
stateTransitions.add(transition.withDestination(successor));
if (states.add(successor)) {
queue.add(successor);
......
......@@ -24,5 +24,7 @@ public interface HistoryGame<S> {
S state();
Formula goal(Agent agent);
HistoryGame<S> game();
}
}
......@@ -7,7 +7,7 @@ import java.util.stream.Stream;
import owl.ltl.Formula;
public record MockHistoryGame<S>(ConcurrentGame<S> concurrentGame) implements HistoryGame<S> {
record MockHistoryState<S>(S state) implements HistoryGame.HistoryState<S> {
record MockHistoryState<S>(S state, MockHistoryGame<S> game) implements HistoryGame.HistoryState<S> {
@Override
public Formula goal(Agent agent) {
return agent.goal();
......@@ -21,11 +21,11 @@ public record MockHistoryGame<S>(ConcurrentGame<S> concurrentGame) implements Hi
@Override
public HistoryState<S> initialState() {
return new MockHistoryState<>(this.concurrentGame.initialState());
return new MockHistoryState<>(this.concurrentGame.initialState(), this);
}
@Override
public Stream<Transition<HistoryState<S>>> transitions(HistoryState<S> state) {
return concurrentGame.transitions(state.state()).stream().map(Transition.transform(MockHistoryState::new));
return concurrentGame.transitions(state.state()).stream().map(Transition.transform(s -> new MockHistoryState<>(s, this)));
}
}
......@@ -5,7 +5,9 @@ import com.cges.graph.HistoryGame.HistoryState;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.PayoffAssignment;
import com.cges.output.DotFormatted;
import java.util.BitSet;
import java.util.Comparator;
import java.util.EnumSet;
import java.util.HashMap;
import java.util.List;
......@@ -20,6 +22,7 @@ import java.util.stream.Stream;
import owl.automaton.Automaton;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.edge.Edge;
import owl.ltl.BooleanConstant;
import owl.ltl.Conjunction;
import owl.ltl.LabelledFormula;
import owl.ltl.rewriter.LiteralMapper;
......@@ -113,10 +116,36 @@ public final class RunGraph<S> {
return suspectGame;
}
public record RunState<S>(Object automatonState, HistoryState<S> historyState) {
public List<String> automatonPropositions() {
return automaton.atomicPropositions();
}
public record RunState<S>(Object automatonState, HistoryState<S> historyState) implements DotFormatted {
@Override
public String toString() {
return "(%s x %s)".formatted(historyState, automatonState);
}
@Override
public String dotString() {
ConcurrentGame<S> game = historyState.game().concurrentGame();
var goalsString = game.agents().stream()
.sorted(Comparator.comparing(Agent::name))
.filter(a -> !historyState.goal(a).equals(BooleanConstant.TRUE))
.map(a -> {
var goalString = LabelledFormula.of(historyState.goal(a), game.atomicPropositions()).toString();
int goalLength = goalString.length();
return goalLength < 20
? goalString
: "%s...%s".formatted(goalString.substring(0, 7), goalString.substring(goalLength - 7));
}).collect(Collectors.joining(",", "[", "]"));
var automatonString = DotFormatted.toString(automatonState);
int automatonLength = automatonString.length();
if (automatonLength > 20) {
automatonString = "%s...%s".formatted(automatonString.substring(0, 7), automatonString.substring(automatonLength - 7));
}
return "%s: %s x %s".formatted(DotFormatted.toString(historyState.state()), goalsString, automatonString);
}
}
}
package com.cges.output;
import java.util.List;
import java.util.Optional;
import java.util.regex.Pattern;
import owl.collections.Either;
import owl.ltl.Formula;
import owl.ltl.LabelledFormula;
import owl.ltl.rewriter.SimplifierRepository;
public interface DotFormatted {
String dotString();
static String toString(Object object) {
if (object instanceof Optional<?> optional) {
return optional.map(DotFormatted::toString).orElse("/");
}
if (object instanceof Either<?,?> either) {
return either.map(DotFormatted::toString, DotFormatted::toString);
}
if (object instanceof LabelledFormula formula) {
return SimplifierRepository.SYNTACTIC_FIXPOINT.apply(formula).toString();
}
if (object instanceof Formula formula) {
return SimplifierRepository.SYNTACTIC_FIXPOINT.apply(formula).toString();
}
return (object instanceof DotFormatted format) ? format.dotString() : object.toString();
}
static String toString(Object object, List<String> propositions) {
if (object instanceof Optional<?> optional) {
return optional.map(o -> toString(o, propositions)).orElse("/");
}
if (object instanceof Either<?,?> either) {
return either.map(o -> toString(o, propositions), o -> toString(o, propositions));
}
if (object instanceof LabelledFormula formula) {
return SimplifierRepository.SYNTACTIC_FIXPOINT.apply(formula).toString();
}
if (object instanceof Formula formula) {
return LabelledFormula.of(SimplifierRepository.SYNTACTIC_FIXPOINT.apply(formula), propositions).toString();
}
return (object instanceof DotFormatted format) ? format.dotString() : object.toString();
}
static String toRecordString(String string) {
var pattern = Pattern.compile("([|{}])");
return pattern.matcher(string).replaceAll("\\\\$1");
}
}
package com.cges.output;
import com.cges.GameSolution;
import com.cges.graph.HistoryGame;
import com.cges.graph.HistoryGame.HistoryState;
import com.cges.graph.RunGraph;
......@@ -7,7 +8,6 @@ import com.cges.graph.SuspectGame;
import com.cges.model.Action;
import com.cges.model.Agent;
import com.cges.model.ConcurrentGame;
import com.cges.model.EquilibriumStrategy;
import com.cges.model.Move;
import com.cges.parity.ParityGame;
import com.cges.parity.Player;
......@@ -15,11 +15,11 @@ 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.HashMap;
import java.util.List;
import java.util.Map;
......@@ -31,6 +31,8 @@ import java.util.stream.Collectors;
import java.util.stream.Stream;
import javax.annotation.Nullable;
import owl.bdd.BddSet;
import owl.ltl.BooleanConstant;
import owl.ltl.LabelledFormula;
public final class DotWriter {
private DotWriter() {}
......@@ -212,37 +214,56 @@ public final class DotWriter {
writer.append("}");
}
public static <S> void writeSolution(SuspectGame<S> suspectGame, RunGraph<S> runGraph, EquilibriumStrategy<S> strategy,
PrintStream writer) {
Object2IntMap<RunGraph.RunState<S>> ids = new Object2IntOpenHashMap<>();
// TODO
public static <S> void writeSolution(GameSolution<S> solution, PrintStream writer) {
var suspectGame = solution.suspectGame();
var strategy = solution.strategy();
var runGraph = solution.runGraph();
List<String> atomicPropositions = suspectGame.historyGame().concurrentGame().atomicPropositions();
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());
*/
Stream.concat(loopStates.stream(), successors.stream()).forEach(runState -> {
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);
// TODO Automaton state labels
writer.append("S_%d [label=\"{%s}\"]\n".formatted(id,
DotFormatted.toString(runState)));
HistoryState<S> historyState = runState.historyState();
String label = Stream.concat(Stream.concat(Stream.of(DotFormatted.toRecordString(DotFormatted.toString(historyState.state()))),
suspectGame.historyGame().concurrentGame().agents().stream()
.filter(a -> !historyState.goal(a).equals(BooleanConstant.TRUE))
.map(a -> "%s %s".formatted(
DotFormatted.toRecordString(a.name()),
DotFormatted.toRecordString(LabelledFormula.of(historyState.goal(a), atomicPropositions).toString())))),
Stream.of(DotFormatted.toRecordString(DotFormatted.toString(runState.automatonState(), runGraph.automatonPropositions()))))
.collect(Collectors.joining("|", "{", "}"));
writer.append("S_%d [shape=record,label=\"%s\"]\n".formatted(id, label));
});
// oddStrategy.lasso().states(false).forEach(runState -> {
// int id = ids.getInt(runState);
// Move move = oddStrategy.moves().get(runState);
// SuspectGame.AdamState<S> adamSuccessor = new SuspectGame.AdamState<>(runState, move);
// Collection<SuspectGame.EveState<S>> eveSuccessors = suspectGame.successors(adamSuccessor);
//
// runGraph.transitions(runState).forEach(transition ->
// writer.append("S_%d -> S_%d [color=%s,label=\"%s\"];\n".formatted(id, ids.getInt(transition.eveSuccessor()),
// eveSuccessors.contains(transition.eveSuccessor().eveState()) ? "green" : "gray",
// DotFormatted.toString(transition.move()))));
// });
strategy.lasso().states(false).forEach(runState -> {
int id = ids.getInt(runState);
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()
.orElseThrow();
writer.append("S_%d -> S_%d [label=\"%s\"];\n".formatted(id, ids.getInt(runSuccessor), DotFormatted.toString(move)));
/*
runGraph.transitions(runState).forEach(transition ->
writer.append("S_%d -> S_%d [color=%s,label=\"%s\"];\n".formatted(id, ids.getInt(transition.successor()),
eveSuccessors.contains(transition.successor().historyState()) ? "green" : "gray",
DotFormatted.toString(move))));
*/
});
writer.append("}");
}
......
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