für vier Felder und zwei Spielmodi
Erstellt von Jonathan Best für die Fachschaft Mathe/Info am KIT im April 2011 und das Paintball-Feld in Haguenau
- Alle Anweisungen auf einer 64-bit Maschine mit schnellem Prozessor und viel RAM (8 GB) ausführen
- Alloy Analyzer, also "alloy4.2-rc.jar" oder eine spätere Version (sofern kompatibel) laden und ausführen
- Mit Alloy Analyzer die Datei "paintball-turnierplan2.als" laden
- Anzahl der Spielbegegnungen berechnen: count(Match) = (count(Teams)^2 - count(Teams))/2
- Die letzte Zeile "run Test for 5 int ..." mit den gewünschten Parametern befüllen, also beispielsweise "run Test for 5 int, exactly 13 Team, exactly 21 Round, exactly 78 Match" wobei der Zahlenwert für "Round" ein Schätzwert ist. Wer mehr Zeit als dieser Verfasser hat, kann auch den Parameter "exactly" vor "Round" weglassen und erhält damit eine Lösung mit 21 Runden oder weniger.
- Im Menü "Options" die Punkte "Maximum Memory to use" und "Maximum Stack to use" erhöhen
- Im Menü "Execute" den Befehl "Run Test ..." ausführen.
- Kaffee trinken gehen
- Bei Fehler: Siehe "Fehlerliste"
- Zwei bis vier Stunden warten
- Bei "Instance found. Predicate is consistent." auf "Instance" klicken. Ein neues Fenster öffnet sich.
- Im Menü "File" auf "Export To"-"XML..." klicken und speichern
- XML-Datei und Anzeige in Alloy in Turnierplan überführen
- ???
- Profit!
Fehler: "No instance found. Predicate may be inconsistent." Lösung: Fehlerhaften Parameter oder Fact finden und korrigieren
Fehler: Gewählter Satsolver crasht Lösung: Sat4J wählen oder Im Menü "Options" die Punkte "Maximum Memory to use" und "Maximum Stack to use" verringern
Fehler: Integer-Überläufe (Lösung enthält negative Zahlen an unerwarteten Stellen) Lösung: In der "Run"-Zeile die Integer-Breite (Parameter "int") erhöhen (default: 4)