Commit 7669383e authored by Tobias MEGGENDORFER's avatar Tobias MEGGENDORFER
Browse files

Init

parents
.gradle
/build/
!gradle-wrapper.jar
.gradletasknamecache
.idea
*.iml
*.ipr
*.iws
/out/
\ No newline at end of file
plugins {
java
distribution
application
idea
}
group = "org.game"
version = "0.1"
java {
sourceCompatibility = JavaVersion.VERSION_17
targetCompatibility = JavaVersion.VERSION_17
withSourcesJar()
withJavadocJar()
}
var defaultEncoding = "UTF-8"
tasks.withType<JavaCompile> { options.encoding = defaultEncoding }
tasks.withType<Javadoc> { options.encoding = defaultEncoding }
tasks.withType<Test> { systemProperty("file.encoding", "UTF-8") }
idea {
module {
isDownloadJavadoc = true
isDownloadSources = true
}
}
repositories {
mavenCentral()
}
dependencies {
// Owl
implementation(files("lib/owl-20.06.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")
implementation("org.antlr", "antlr4-runtime", "4.8")
// Z3
implementation("io.github.tudo-aqua", "z3-turnkey", "4.8.14")
// Guava
implementation("com.google.guava", "guava", "31.0.1-jre")
// https://mvnrepository.com/artifact/info.picocli/picocli
implementation("info.picocli", "picocli", "4.6.3")
}
application {
mainClass.set("com.cges.Main")
applicationDefaultJvmArgs = listOf("-ea")
}
distributionUrl=https\://services.gradle.org/distributions/gradle-7.4-bin.zip
distributionBase=GRADLE_USER_HOME
distributionPath=wrapper/dists
zipStorePath=wrapper/dists
zipStoreBase=GRADLE_USER_HOME
#!/usr/bin/env sh
##############################################################################
##
## Gradle start up script for UN*X
##
##############################################################################
# Attempt to set APP_HOME
# Resolve links: $0 may be a link
PRG="$0"
# Need this for relative symlinks.
while [ -h "$PRG" ] ; do
ls=`ls -ld "$PRG"`
link=`expr "$ls" : '.*-> \(.*\)$'`
if expr "$link" : '/.*' > /dev/null; then
PRG="$link"
else
PRG=`dirname "$PRG"`"/$link"
fi
done
SAVED="`pwd`"
cd "`dirname \"$PRG\"`/" >/dev/null
APP_HOME="`pwd -P`"
cd "$SAVED" >/dev/null
APP_NAME="Gradle"
APP_BASE_NAME=`basename "$0"`
# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
DEFAULT_JVM_OPTS=""
# Use the maximum available, or set MAX_FD != -1 to use that value.
MAX_FD="maximum"
warn () {
echo "$*"
}
die () {
echo
echo "$*"
echo
exit 1
}
# OS specific support (must be 'true' or 'false').
cygwin=false
msys=false
darwin=false
nonstop=false
case "`uname`" in
CYGWIN* )
cygwin=true
;;
Darwin* )
darwin=true
;;
MINGW* )
msys=true
;;
NONSTOP* )
nonstop=true
;;
esac
CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar
# Determine the Java command to use to start the JVM.
if [ -n "$JAVA_HOME" ] ; then
if [ -x "$JAVA_HOME/jre/sh/java" ] ; then
# IBM's JDK on AIX uses strange locations for the executables
JAVACMD="$JAVA_HOME/jre/sh/java"
else
JAVACMD="$JAVA_HOME/bin/java"
fi
if [ ! -x "$JAVACMD" ] ; then
die "ERROR: JAVA_HOME is set to an invalid directory: $JAVA_HOME
Please set the JAVA_HOME variable in your environment to match the
location of your Java installation."
fi
else
JAVACMD="java"
which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
Please set the JAVA_HOME variable in your environment to match the
location of your Java installation."
fi
# Increase the maximum file descriptors if we can.
if [ "$cygwin" = "false" -a "$darwin" = "false" -a "$nonstop" = "false" ] ; then
MAX_FD_LIMIT=`ulimit -H -n`
if [ $? -eq 0 ] ; then
if [ "$MAX_FD" = "maximum" -o "$MAX_FD" = "max" ] ; then
MAX_FD="$MAX_FD_LIMIT"
fi
ulimit -n $MAX_FD
if [ $? -ne 0 ] ; then
warn "Could not set maximum file descriptor limit: $MAX_FD"
fi
else
warn "Could not query maximum file descriptor limit: $MAX_FD_LIMIT"
fi
fi
# For Darwin, add options to specify how the application appears in the dock
if $darwin; then
GRADLE_OPTS="$GRADLE_OPTS \"-Xdock:name=$APP_NAME\" \"-Xdock:icon=$APP_HOME/media/gradle.icns\""
fi
# For Cygwin, switch paths to Windows format before running java
if $cygwin ; then
APP_HOME=`cygpath --path --mixed "$APP_HOME"`
CLASSPATH=`cygpath --path --mixed "$CLASSPATH"`
JAVACMD=`cygpath --unix "$JAVACMD"`
# We build the pattern for arguments to be converted via cygpath
ROOTDIRSRAW=`find -L / -maxdepth 1 -mindepth 1 -type d 2>/dev/null`
SEP=""
for dir in $ROOTDIRSRAW ; do
ROOTDIRS="$ROOTDIRS$SEP$dir"
SEP="|"
done
OURCYGPATTERN="(^($ROOTDIRS))"
# Add a user-defined pattern to the cygpath arguments
if [ "$GRADLE_CYGPATTERN" != "" ] ; then
OURCYGPATTERN="$OURCYGPATTERN|($GRADLE_CYGPATTERN)"
fi
# Now convert the arguments - kludge to limit ourselves to /bin/sh
i=0
for arg in "$@" ; do
CHECK=`echo "$arg"|egrep -c "$OURCYGPATTERN" -`
CHECK2=`echo "$arg"|egrep -c "^-"` ### Determine if an option
if [ $CHECK -ne 0 ] && [ $CHECK2 -eq 0 ] ; then ### Added a condition
eval `echo args$i`=`cygpath --path --ignore --mixed "$arg"`
else
eval `echo args$i`="\"$arg\""
fi
i=$((i+1))
done
case $i in
(0) set -- ;;
(1) set -- "$args0" ;;
(2) set -- "$args0" "$args1" ;;
(3) set -- "$args0" "$args1" "$args2" ;;
(4) set -- "$args0" "$args1" "$args2" "$args3" ;;
(5) set -- "$args0" "$args1" "$args2" "$args3" "$args4" ;;
(6) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" ;;
(7) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" ;;
(8) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" "$args7" ;;
(9) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" "$args7" "$args8" ;;
esac
fi
# Escape application args
save () {
for i do printf %s\\n "$i" | sed "s/'/'\\\\''/g;1s/^/'/;\$s/\$/' \\\\/" ; done
echo " "
}
APP_ARGS=$(save "$@")
# Collect all arguments for the java command, following the shell quoting and substitution rules
eval set -- $DEFAULT_JVM_OPTS $JAVA_OPTS $GRADLE_OPTS "\"-Dorg.gradle.appname=$APP_BASE_NAME\"" -classpath "\"$CLASSPATH\"" org.gradle.wrapper.GradleWrapperMain "$APP_ARGS"
# by default we should be in the correct project dir, but when run from Finder on Mac, the cwd is wrong
if [ "$(uname)" = "Darwin" ] && [ "$HOME" = "$PWD" ]; then
cd "$(dirname "$0")"
fi
exec "$JAVACMD" "$@"
@if "%DEBUG%" == "" @echo off
@rem ##########################################################################
@rem
@rem Gradle startup script for Windows
@rem
@rem ##########################################################################
@rem Set local scope for the variables with windows NT shell
if "%OS%"=="Windows_NT" setlocal
set DIRNAME=%~dp0
if "%DIRNAME%" == "" set DIRNAME=.
set APP_BASE_NAME=%~n0
set APP_HOME=%DIRNAME%
@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
set DEFAULT_JVM_OPTS=
@rem Find java.exe
if defined JAVA_HOME goto findJavaFromJavaHome
set JAVA_EXE=java.exe
%JAVA_EXE% -version >NUL 2>&1
if "%ERRORLEVEL%" == "0" goto init
echo.
echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
echo.
echo Please set the JAVA_HOME variable in your environment to match the
echo location of your Java installation.
goto fail
:findJavaFromJavaHome
set JAVA_HOME=%JAVA_HOME:"=%
set JAVA_EXE=%JAVA_HOME%/bin/java.exe
if exist "%JAVA_EXE%" goto init
echo.
echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
echo.
echo Please set the JAVA_HOME variable in your environment to match the
echo location of your Java installation.
goto fail
:init
@rem Get command-line arguments, handling Windows variants
if not "%OS%" == "Windows_NT" goto win9xME_args
:win9xME_args
@rem Slurp the command line arguments.
set CMD_LINE_ARGS=
set _SKIP=2
:win9xME_args_slurp
if "x%~1" == "x" goto execute
set CMD_LINE_ARGS=%*
:execute
@rem Setup the command line
set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar
@rem Execute Gradle
"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %CMD_LINE_ARGS%
:end
@rem End local scope for the variables with windows NT shell
if "%ERRORLEVEL%"=="0" goto mainEnd
:fail
rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of
rem the _cmd.exe /c_ return code!
if not "" == "%GRADLE_EXIT_CONSOLE%" exit 1
exit /b 1
:mainEnd
if "%OS%"=="Windows_NT" endlocal
:omega
rootProject.name = "cges"
package com.cges;
import com.cges.algorithm.BoundedChecker;
import com.cges.algorithm.SuspectSolver;
import com.cges.model.ConcurrentGame;
import com.cges.model.RunGraph;
import com.cges.model.SuspectGame;
import com.google.common.base.Stopwatch;
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 {
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 = BoundedChecker.checkScc(runGraph);
System.out.println("Lasso: " + stopwatch);
System.out.println(lasso.size());
System.out.println(lasso);
}
}
}
package com.cges.algorithm;
import static com.google.common.base.Preconditions.checkNotNull;
import static com.google.common.base.Preconditions.checkState;
import com.cges.model.RunGraph;
import com.cges.model.RunGraph.State;
import com.google.common.collect.Lists;
import com.google.common.collect.Sets;
import com.microsoft.z3.BitVecExpr;
import com.microsoft.z3.BitVecNum;
import com.microsoft.z3.BitVecSort;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.BoolSort;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.Model;
import com.microsoft.z3.SeqSort;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;
import com.microsoft.z3.Z3Exception;
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.logging.Level;
import java.util.logging.Logger;
import java.util.stream.Collectors;
import java.util.stream.IntStream;
import owl.automaton.algorithm.SccDecomposition;
public final class BoundedChecker {
private record SccPair(Set<State> scc, Set<State> accepting) {}
private static final Logger logger = Logger.getLogger(BoundedChecker.class.getName());
private BoundedChecker() {}
public static List<State> checkScc(RunGraph graph) {
Set<State> acceptingStates = graph.states().stream().filter(State::accepting).collect(Collectors.toSet());
List<SccPair> sccs = SccDecomposition.of(graph.initialStates(), graph::successors).sccsWithoutTransient()
.stream()
.map(scc -> new SccPair(scc, Set.copyOf(Sets.intersection(scc, acceptingStates))))
.filter(pair -> !pair.accepting().isEmpty())
.toList();
Set<State> statesInAcceptingSccs = sccs.stream().map(SccPair::scc).flatMap(Collection::stream).collect(Collectors.toSet());
List<State> path = new ArrayList<>();
{
Set<State> states = new HashSet<>(graph.initialStates());
Queue<State> queue = new ArrayDeque<>(states);
Map<State, State> predecessor = new HashMap<>();
while (!queue.isEmpty()) {
State current = queue.poll();
if (statesInAcceptingSccs.contains(current)) {
while (current != null) {
path.add(current);
current = predecessor.get(current);
}
break;
}
for (State successor : graph.successors(current)) {
if (states.add(successor)) {
predecessor.put(successor, current);
queue.add(successor);
}
}
}
}
if (path.isEmpty()) {
return path;
}
State recurrentState = path.get(0);
SccPair scc = sccs.stream().filter(pair -> pair.scc().contains(recurrentState)).findAny().orElseThrow();
List<State> sccPath = new ArrayList<>();
{
Set<State> states = new HashSet<>(List.of(recurrentState));
Queue<State> queue = new ArrayDeque<>(states);
Map<State, State> predecessor = new HashMap<>();
while (!queue.isEmpty()) {
State current = queue.poll();
if (current.accepting()) {
while (current != null) {
sccPath.add(current);
current = predecessor.get(current);
}
break;
}
for (State successor : Sets.intersection(graph.successors(current), scc.scc())) {
if (states.add(successor)) {
predecessor.put(successor, current);
queue.add(successor);
}
}
}
}
State acceptingState = sccPath.get(0);
List<State> sccRecurrentPath = new ArrayList<>();
{
Set<State> states = new HashSet<>(List.of(acceptingState));
Queue<State> queue = new ArrayDeque<>(states);
Map<State, State> predecessor = new HashMap<>();
while (!queue.isEmpty()) {
State current = queue.poll();
if (current.equals(acceptingState)) {
while (current != null) {
sccRecurrentPath.add(current);
current = predecessor.get(current);
}
break;
}
for (State successor : Sets.intersection(graph.successors(current), scc.scc())) {
if (states.add(successor)) {
predecessor.put(successor, current);
queue.add(successor);
}
}
}
}
List<State> loop = new ArrayList<>();
loop.addAll(sccRecurrentPath);
loop.addAll(sccPath);
loop.addAll(path);
return Lists.reverse(loop);
}
@SuppressWarnings("unchecked")
public static List<State> check(RunGraph graph) {
// TODO Derive upper bound on depth from graph
// TODO QBF or similar instead of bit encoding
Set<State> acceptingStates = graph.states().stream().filter(State::accepting).collect(Collectors.toSet());
if (acceptingStates.isEmpty()) {
return List.of();
}
// TODO Better bound on the largest loop -- most distant scc
int depth = graph.size();
int bits = (int) Math.ceil(StrictMath.log(graph.size()) / StrictMath.log(2));
try (Context ctx = new Context()) {
BoolExpr[][] variables = new BoolExpr[depth + 1][bits];
for (int step = 0; step <= depth; step++) {
for (int bit = 0; bit < bits; bit++) {
variables[step][bit] = ctx.mkBoolConst("v_%d_%d".formatted(step, bit));
}
}
List<State> stateNumbering = List.copyOf(graph.states());
@SuppressWarnings("unchecked")
Map<State, BoolExpr>[] stepStateExpressions = new Map[depth + 1];
Arrays.setAll(stepStateExpressions, i -> new HashMap<>());
ListIterator<State> iterator = stateNumbering.listIterator();
while (iterator.hasNext()) {
int index = iterator.nextIndex();
State state = iterator.next();
for (int step = 0; step <= depth; step++) {
BoolExpr[] stepVariables = variables[step];
BoolExpr[] bitExpression = new BoolExpr[bits];
Arrays.setAll(bitExpression, bit -> (index & (1 << bit)) == 0 ? ctx.mkNot(stepVariables[bit]) : stepVariables[bit]);
stepStateExpressions[step].put(state, ctx.mkAnd(bitExpression));
}
}
Solver solver = ctx.mkSolver("QF_FD");
solver.add(ctx.mkOr(graph.initialStates().stream()
.map(stepStateExpressions[0]::get).toArray(BoolExpr[]::new)).simplify());
List<State> lasso = new ArrayList<>(depth + 1);
for (int k = 1; k <= depth; k++) {
logger.log(Level.FINE, "Building model for depth {0}", k);
int cutoff = k;
solver.add(ctx.mkAnd(graph.states().stream().map(state -> {
var successors = graph.successors(state);
return ctx.mkImplies(stepStateExpressions[cutoff - 1].get(state),
ctx.mkOr(successors.stream().map(stepStateExpressions[cutoff]::get).toArray(BoolExpr[]::new)));
}).toArray(BoolExpr[]::new)).simplify());
Expr<BoolSort>[] acceptingLoopAtStep = new Expr[cutoff + 1];
// Can we use SCCs here?
Arrays.setAll(acceptingLoopAtStep, step -> {
BoolExpr[] loopExpr = new BoolExpr[bits];
Arrays.setAll(loopExpr, i -> ctx.mkEq(variables[step][i], variables[cutoff][i]));
Expr<BoolSort> loop = ctx.mkAnd(loopExpr).simplify();
Expr<BoolSort> visitAcceptingState = ctx.mkOr(IntStream.range(step, cutoff)
.mapToObj(i -> ctx.mkOr(acceptingStates.stream().map(stepStateExpressions[i]::get).toArray(BoolExpr[]::new)).simplify())
.toArray(Expr[]::new));
return ctx.mkAnd(loop, visitAcceptingState);
});
Expr<BoolSort> acceptingLassoExpression = ctx.mkOr(acceptingLoopAtStep).simplify();
Status check = solver.check(acceptingLassoExpression);
if (check == Status.UNKNOWN) {
throw new Z3Exception("Status unknown");
}
if (check == Status.UNSATISFIABLE) {
continue;
}
Model model = solver.getModel();
boolean[][] valuation = new boolean[cutoff + 1][bits];
for (int step = 0; step <= cutoff; step++) {
for (int bit = 0; bit < bits; bit++) {
Expr<BoolSort> z3valuation = model.eval(variables[step][bit], false);