Commit 346051ee authored by Tobias MEGGENDORFER's avatar Tobias MEGGENDORFER
Browse files

Input formats and preliminary strategy extraction

parent e853f9c0
......@@ -3,6 +3,7 @@ plugins {
distribution
application
idea
antlr
}
group = "org.game"
......@@ -38,20 +39,33 @@ dependencies {
implementation("de.tum.in", "jbdd", "0.5.2")
implementation("de.tum.in", "naturals-util", "0.16.0")
implementation("commons-cli", "commons-cli", "1.4")
implementation("org.antlr", "antlr4-runtime", "4.8")
implementation("org.antlr", "antlr4-runtime", "4.8-1")
// Z3
implementation("io.github.tudo-aqua", "z3-turnkey", "4.8.14")
// https://mvnrepository.com/artifact/com.google.code.gson/gson
implementation("com.google.code.gson", "gson", "2.9.0")
// Guava
implementation("com.google.guava", "guava", "31.0.1-jre")
// https://mvnrepository.com/artifact/info.picocli/picocli
implementation("info.picocli", "picocli", "4.6.3")
antlr("org.antlr", "antlr4", "4.8-1")
}
configurations {
api { setExtendsFrom(extendsFrom.filter { it.name != "antlr" }) }
}
application {
mainClass.set("com.cges.Main")
applicationDefaultJvmArgs = listOf("-ea")
}
tasks.generateGrammarSource {
arguments.addAll(listOf("-visitor", "-long-messages", "-lib", "src/main/antlr"))
outputDirectory = outputDirectory.resolve("com/cges/grammar")
}
{
"name": "gossip2",
"ap": [
"g1",
"g2"
],
"modules": {
"A1": {
"goal": "G F g1",
"payoff": true,
"actions": ["a", "g", "w"],
"labels": ["g1"],
"initial": "s11",
"states": {
"s11": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s11"
},
{
"action": "g",
"guard": "true",
"to": "s12"
}
]
},
"s12": {
"labels": ["g1"],
"transitions": [
{
"action": "w",
"guard": "!g2",
"to": "s12"
},
{
"action": "a",
"guard": "g2",
"to": "s11"
}
]
}
}
},
"A2": {
"goal": "G F g2",
"payoff": true,
"actions": ["a", "g", "w"],
"labels": ["g2"],
"initial": "s21",
"states": {
"s21": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s21"
},
{
"action": "g",
"guard": "true",
"to": "s22"
}
]
},
"s22": {
"labels": ["g2"],
"transitions": [
{
"action": "w",
"guard": "!g1",
"to": "s22"
},
{
"action": "a",
"guard": "g1",
"to": "s21"
}
]
}
}
}
}
}
\ No newline at end of file
{
"name": "gossip2",
"ap": [
"g1",
"g2",
"g3"
],
"modules": {
"A1": {
"goal": "G F g1",
"payoff": true,
"actions": [
"a",
"g",
"w"
],
"labels": [
"g1"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s2"
}
]
},
"s2": {
"labels": [
"g1"
],
"transitions": [
{
"action": "w",
"guard": "!g2 & !g3",
"to": "s2"
},
{
"action": "a",
"guard": "g2 | g3",
"to": "s1"
}
]
}
}
},
"A2": {
"goal": "G F g2",
"payoff": true,
"actions": [
"a",
"g",
"w"
],
"labels": [
"g2"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s2"
}
]
},
"s2": {
"labels": [
"g2"
],
"transitions": [
{
"action": "w",
"guard": "!g1 & !g3",
"to": "s2"
},
{
"action": "a",
"guard": "g1 | g3",
"to": "s1"
}
]
}
}
},
"A3": {
"goal": "G F g3",
"payoff": true,
"actions": [
"a",
"g",
"w"
],
"labels": [
"g3"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s2"
}
]
},
"s2": {
"labels": [
"g3"
],
"transitions": [
{
"action": "w",
"guard": "!g1 & !g2",
"to": "s2"
},
{
"action": "a",
"guard": "g1 | g2",
"to": "s1"
}
]
}
}
}
}
}
\ No newline at end of file
{
"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
lexer grammar PropositionalLexer;
@lexer::header {
package com.cges.grammar;
}
TRUE : 'tt' | 'true' | '1';
FALSE : 'ff' | 'false' | '0';
NOT : '!' | 'NOT';
IMP : '->' | '-->' | '=>' | '==>' | 'IMP';
BIIMP : '<->' | '<=>' | 'BIIMP';
XOR : '^' | 'XOR' | 'xor';
AND : '&&' | '&' | 'AND' ;
OR : '||' | '|' | 'OR' ;
LPAREN : '(';
RPAREN : ')';
LDQUOTE : '"' -> mode(DOUBLE_QUOTED);
LSQUOTE : '\'' -> mode(SINGLE_QUOTED);
VARIABLE : [a-zA-Z_0-9]+;
ERROR : . ;
fragment
WHITESPACE : [ \t\n\r\f]+;
SKIP_DEF : WHITESPACE -> skip;
mode DOUBLE_QUOTED;
RDQUOTE : '"' -> mode(DEFAULT_MODE);
DOUBLE_QUOTED_VARIABLE : ~["]+;
mode SINGLE_QUOTED;
RSQUOTE : '\'' -> mode(DEFAULT_MODE);
SINGLE_QUOTED_VARIABLE : ~[']+;
parser grammar PropositionalParser;
options {
language = Java;
tokenVocab = PropositionalLexer;
}
@header {
package com.cges.grammar;
}
formula
: root=expression EOF
;
expression
: or=orExpression
;
orExpression
: andExpression (OR andExpression)*
;
andExpression
: binaryExpression (AND binaryExpression)*
;
binaryExpression
: left=unaryExpression op=binaryOp right=binaryExpression # binaryOperation
| unaryExpression # binaryUnary
;
unaryExpression
: op=unaryOp inner=binaryExpression # unaryOperation
| atomExpression # unaryAtom
;
atomExpression
: constant=bool # boolean
| variable=VARIABLE # variable
| LSQUOTE variable=SINGLE_QUOTED_VARIABLE RSQUOTE # variable
| LDQUOTE variable=DOUBLE_QUOTED_VARIABLE RDQUOTE # variable
| LPAREN nested=expression RPAREN # nested
;
unaryOp
: NOT
;
binaryOp
: BIIMP | IMP | XOR
;
bool
: TRUE | FALSE
;
package com.cges;
import static com.google.common.base.Preconditions.checkState;
import com.cges.algorithm.HistoryGame;
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.ConcurrentGame;
import com.cges.model.RunGraph;
import com.cges.model.SuspectGame;
import com.cges.output.DotWriter;
import com.cges.parser.ExplicitParser;
import com.cges.parser.GameParser;
import com.cges.parser.ModuleParser;
import com.google.common.base.Stopwatch;
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.List;
import java.util.Set;
public class Main {
public static void main(String[] args) throws IOException {
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]);
}
analyse(game);
}
private static <S> void analyse(ConcurrentGame<S> game) {
Stopwatch stopwatch = Stopwatch.createStarted();
try (BufferedReader reader = Files.newBufferedReader(Path.of(args[0]))) {
ConcurrentGame parse = ConcurrentGame.parse(reader.lines());
System.out.println("Parsing: " + stopwatch);
SuspectGame suspectGame = SuspectGame.create(parse);
System.out.println("Suspect: " + stopwatch);
Set<SuspectGame.EveState> winningEveStates = SuspectSolver.computeWinningEveStates(suspectGame);
System.out.println("Winning: " + stopwatch);
RunGraph runGraph = RunGraph.create(suspectGame, winningEveStates);
System.out.println("Run: " + stopwatch);
List<RunGraph.State> lasso = RunGraphSccSolver.solve(runGraph);
System.out.println("Lasso: " + stopwatch);
checkState(runGraph.isAcceptingLasso(lasso));
System.out.println(lasso.size());
System.out.println(lasso);
var suspectGame = SuspectGame.create(new HistoryGame<>(game));
System.out.println("Suspect: " + stopwatch);
var suspectSolution = SuspectSolver.computeWinningEveStates(suspectGame);
System.out.println("Winning: " + stopwatch);
var runGraph = RunGraph.create(suspectGame, suspectSolution);
System.out.println("Run: " + stopwatch);
var lasso = RunGraphSccSolver.solve(runGraph);
System.out.println("Lasso: " + stopwatch);
if (lasso.isPresent()) {
var strategy = StrategyMapper.createStrategy(suspectGame, suspectSolution, lasso.get());
DotWriter.writeSolution(suspectGame, runGraph, strategy, System.out);
}
}
}
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;
import com.google.common.collect.Lists;
import de.tum.in.naturals.Indices;
import java.util.BitSet;
import java.util.Comparator;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Objects;
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 HistoryGame<S> {
public interface HistoryState<S> {
S state();
Formula goal(Agent agent);
}
static final class ListHistoryState<S> implements HistoryState<S> {
private final S state;
private final List<EquivalenceClass> agentGoals;