-
Notifications
You must be signed in to change notification settings - Fork 0
/
solver.py
67 lines (57 loc) · 2.53 KB
/
solver.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
import argparse
import os
from arena.load_arena import load_arena, load_arena_parity
from tools.output import print_results, save_results
from solvers.reachability import reachability_solver
from solvers.safety import safety_solver
from solvers.buchi import buchi_solver
from solvers.cobuchi import cobuchi_solver
from solvers.parity import parity_solver_strategy
# Create the parser
my_parser = argparse.ArgumentParser(description='Solver for different types of games on graphs')
# Add the arguments
my_parser.add_argument('--game', type=str, required=False, help="The type of game to be solved")
my_parser.add_argument('--arena', type=str, default="assets/arenawiki.txt", help="Path to the arena txt file")
my_parser.add_argument('--target', type=int, nargs='+', default=None, help="Target set for the game")
# Execute the parse_args() method
args = my_parser.parse_args()
# Extract the name of the arena from the path
arena_name = os.path.basename(args.arena)
# Reachability solver
if args.game == "reachability":
arena = load_arena(args.arena)
R = args.target or [4, 5]
print("Reachability set =", R)
win0, strat0, win1, strat1 = reachability_solver(arena, R)
print_results("Reachability", win0, win1, strat0, strat1)
save_results("Reachability", arena_name, win0, win1, strat0, strat1)
# Safety Solver
elif args.game == "safety":
arena = load_arena(args.arena)
S = args.target or [1, 2, 3, 4, 5, 7, 8]
print("Safety set =", S)
win0, strat0, win1, strat1 = safety_solver(arena, S)
print_results("Safety", win0, win1, strat0, strat1)
save_results("Safety", arena_name, win0, win1, strat0, strat1)
# Buchi solver
elif args.game == "buchi":
arena = load_arena(args.arena)
F = args.target or [4, 6]
print("Recurrence set =", F)
win0, strat0, win1, strat1 = buchi_solver(arena, F)
print_results("Buchi", win0, win1, strat0, strat1)
save_results("Buchi", arena_name, win0, win1, strat0, strat1)
# Co-buchi solver
elif args.game == "cobuchi":
arena = load_arena(args.arena)
C = args.target or [2, 4, 5, 6, 7, 8]
print("Persistence set =", C)
win0, strat0, win1, strat1 = cobuchi_solver(arena, C)
print_results("Co-buchi", win0, win1, strat0, strat1)
save_results("Co-buchi", arena_name, win0, win1, strat0, strat1)
# Parity solver
elif args.game == "parity":
arena = load_arena_parity(args.arena)
win0, win1, strat0, strat1 = parity_solver_strategy(arena)
print_results("Parity", win0, win1, strat0, strat1)
save_results("Parity", arena_name, win0, win1, strat0, strat1)