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

More model

parent d8886ead
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -10,8 +10,11 @@ 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;
import com.cges.parser.GameParser;
import com.cges.parser.Module;
import com.cges.parser.ModuleGame;
import com.google.common.base.Stopwatch;
import com.google.common.collect.Sets;
import com.google.gson.JsonArray;
......@@ -49,7 +52,13 @@ public final class Main {
} else {
try (BufferedReader reader = Files.newBufferedReader(Path.of(args[0]))) {
JsonObject jsonObject = JsonParser.parseReader(reader).getAsJsonObject();
game = GameParser.parseExplicit(jsonObject);
game = GameParser.parse(jsonObject);
if (game instanceof ModuleGame<?> module) {
for (Module<?> m : module.modules()) {
DotWriter.writeModule(m, module, System.out);
System.out.println();
}
}
JsonArray validation = jsonObject.getAsJsonArray("expected");
if (validation == null) {
validationSet = null;
......
......@@ -21,7 +21,7 @@ import owl.automaton.algorithm.SccDecomposition;
public final class RunGraphSccSolver {
private RunGraphSccSolver() {}
public static <S> List<RunState<S>> searchShort(RunGraph<S> graph) {
public static <S> List<RunState<S>> search(RunGraph<S> graph) {
List<Set<RunState<S>>> decomposition = SccDecomposition.of(graph.initialStates(), graph::successors).sccsWithoutTransient();
Map<RunState<S>, List<RunState<S>>> shortestAcceptingCycle = new HashMap<>();
......
......@@ -58,7 +58,7 @@ public final class RunGraphSolver {
});
}
var path = RunGraphSccSolver.searchShort(graph);
var path = RunGraphBmcSolver.search(graph);
if (path.isEmpty()) {
return Optional.empty();
}
......
......@@ -16,6 +16,7 @@ import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;
import java.util.stream.IntStream;
import java.util.stream.Stream;
import owl.automaton.Automaton;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.edge.Edge;
......@@ -46,7 +47,8 @@ public final class RunGraph<S> {
Set<Agent> agents = concurrentGame.agents();
LabelledFormula eveGoal = SimplifierRepository.SYNTACTIC_FIXPOINT.apply(LabelledFormula.of(
Conjunction.of(agents.stream().map(a -> payoffAssignment.isLoser(a) ? a.goal().not() : a.goal())),
Conjunction.of(Stream.concat(agents.stream().map(a -> payoffAssignment.isLoser(a) ? a.goal().not() : a.goal()),
Stream.of(suspectGame.historyGame().concurrentGame().goal().formula()))),
concurrentGame.atomicPropositions()));
LiteralMapper.ShiftedLabelledFormula shifted = LiteralMapper.shiftLiterals(eveGoal);
var translator = LtlTranslationRepository.defaultTranslation(
......
......@@ -57,6 +57,10 @@ public final class Agent {
return Objects.requireNonNull(actions.get(name));
}
public boolean hasAction(String name) {
return actions.containsKey(name);
}
public Payoff payoff() {
return payoff;
}
......
......@@ -8,6 +8,7 @@ import java.util.NoSuchElementException;
import java.util.Set;
import java.util.stream.Collectors;
import javax.annotation.Nullable;
import owl.ltl.LabelledFormula;
public interface ConcurrentGame<S> {
String name();
......@@ -35,6 +36,8 @@ public interface ConcurrentGame<S> {
Set<String> labels(S state);
LabelledFormula goal();
Set<S> states();
Set<Transition<S>> transitions(S state);
......
......@@ -4,12 +4,15 @@ import com.cges.graph.HistoryGame;
import com.cges.graph.HistoryGame.HistoryState;
import com.cges.graph.RunGraph;
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;
import com.cges.parser.Module;
import com.cges.parser.ModuleGame;
import com.google.common.collect.HashMultimap;
import com.google.common.collect.SetMultimap;
import it.unimi.dsi.fastutil.objects.Object2IntMap;
......@@ -17,7 +20,9 @@ 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;
import java.util.Queue;
import java.util.Set;
import java.util.function.Function;
......@@ -25,10 +30,44 @@ import java.util.function.Predicate;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import javax.annotation.Nullable;
import owl.bdd.BddSet;
public final class DotWriter {
private DotWriter() {}
public static <S> void writeModule(Module<S> module, ModuleGame<?> game, PrintStream writer) {
Object2IntMap<S> ids = new Object2IntOpenHashMap<>();
module.states().forEach(s -> ids.put(s, ids.size()));
writer.append("digraph {\n");
for (Object2IntMap.Entry<S> entry : ids.object2IntEntrySet()) {
writer.append("MS_%d [label=\"%s\"]\n".formatted(
entry.getIntValue(),
DotFormatted.toString(entry.getKey())
));
}
for (var entry : ids.object2IntEntrySet()) {
S state = entry.getKey();
Map<S, Map<Action, BddSet>> successorByAction = new HashMap<>();
for (Action action : module.actions(state)) {
for (Map.Entry<S, BddSet> transition : module.successorMap(state, action).entrySet()) {
successorByAction.computeIfAbsent(transition.getKey(), k -> new HashMap<>()).merge(action, transition.getValue(), BddSet::union);
}
}
for (var moveEntry : successorByAction.entrySet()) {
String label = moveEntry.getValue().entrySet().stream()
.map(e -> e.getValue().isUniverse()
? e.getKey().name()
: "%s[%s]".formatted(e.getKey().name(), e.getValue().toExpression().map(game.atomicPropositions()::get)))
.collect(Collectors.joining(", "));
writer.append("MS_%d -> MS_%d [label=\"%s\"]\n".formatted(entry.getIntValue(), ids.getInt(moveEntry.getKey()), label));
}
}
writer.append("}");
}
public static <S> void writeHistoryGame(HistoryGame<S> game, PrintStream writer,
@Nullable Predicate<HistoryState<S>> winning) {
Object2IntMap<HistoryState<S>> ids = new Object2IntOpenHashMap<>();
......@@ -67,7 +106,6 @@ public final class DotWriter {
writer.append("}");
}
public static <S> void writeSuspectGame(SuspectGame<S> game, SuspectGame.EveState<S> initial,
PrintStream writer, @Nullable Predicate<SuspectGame.EveState<S>> winning) {
Object2IntMap<SuspectGame.EveState<S>> ids = new Object2IntOpenHashMap<>();
......
......@@ -16,6 +16,8 @@ import java.util.Objects;
import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;
import owl.ltl.BooleanConstant;
import owl.ltl.LabelledFormula;
final class ExplicitGame<S> implements ConcurrentGame<S> {
private final String name;
......@@ -84,6 +86,11 @@ final class ExplicitGame<S> implements ConcurrentGame<S> {
return labels.apply(state);
}
@Override
public LabelledFormula goal() {
return LabelledFormula.of(BooleanConstant.TRUE, atomicPropositions);
}
public static final class MapMove implements Move, DotFormatted {
private final Map<Agent, Action> actions;
private final int hashCode;
......
......@@ -89,7 +89,7 @@ public final class GameParser {
return new ExplicitGame<>("empty", agents, propositions, initialState, states, transitions, state -> Set.of(state.name()));
}
public static ConcurrentGame<?> parseExplicit(JsonObject json) {
public static ConcurrentGame<?> parse(JsonObject json) {
String type = json.getAsJsonPrimitive("type").getAsString();
return switch (type) {
case "module" -> ModuleParser.parse(json);
......
......@@ -3,6 +3,7 @@ package com.cges.parser;
import com.cges.model.Action;
import com.cges.model.Agent;
import java.util.BitSet;
import java.util.Collections;
import java.util.HashMap;
import java.util.Map;
import java.util.Set;
......@@ -53,6 +54,10 @@ public class Module<S> {
return transitions.get(state).get(action).keySet();
}
public Map<S, BddSet> successorMap(S state, Action action) {
return Collections.unmodifiableMap(transitions.get(state).get(action));
}
public Map<Action, S> successors(S state, BitSet valuation) {
Map<Action, S> successors = new HashMap<>();
transitions.get(state).forEach((action, actionTransitions) -> {
......
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