stv/main.py at master · blackbat13/stv · GitHub

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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
import click
import time
import stv.models.asynchronous.template_parser as template_parser
from stv.models.asynchronous.global_model import GlobalModel
from stv.models.asynchronous.parser import GlobalModelParser
from stv.models import TianJiModel, CastleModel, BridgeModel


@click.group()
def run():
    pass


@run.group()
def verify():
    pass


@verify.group()
def synchronous():
    pass


def verify_synchronous(model_generator, imperfect: bool):
    click.echo("Generating model")

    time_start = time.perf_counter()
    model_generator.generate()
    time_end = time.perf_counter()

    click.echo(f"Model generated in {time_end - time_start} seconds")
    click.echo("Starting verification")

    if imperfect:
        click.echo("Imperfect information")
        time_start = time.perf_counter()
        atl_model = model_generator.model.to_atl_imperfect()
        time_end = time.perf_counter()
    else:
        click.echo("Perfect information")
        time_start = time.perf_counter()
        atl_model = model_generator.model.to_atl_perfect()
        time_end = time.perf_counter()

    click.echo(f"Formula verified in {time_end - time_start} seconds")
    winning = model_generator.get_model_winning_states()

    result = atl_model.minimum_formula_many_agents([0], winning)

    if 0 in result:
        click.echo("Approximation result: True")
    else:
        click.echo("Approximation result: False")


@synchronous.command()
@click.option('--horses', type=int, prompt='Number of horses', help='number of horses')
@click.option('--imperfect', is_flag=True, help='imperfect information')
def tianji(horses: int, imperfect: bool):
    click.echo(f"TianJi model, {horses} horses")
    tian_ji_model = TianJiModel(horses)
    verify_synchronous(tian_ji_model, imperfect)


@synchronous.command()
@click.option('--cards', type=int, prompt='Number of cards', help='number of cards')
@click.option('--imperfect', is_flag=True, help='imperfect information')
def bridge(cards: int, imperfect: bool):
    click.echo(f"Bridge model, {cards} cards")
    hands = BridgeModel.generate_random_hands(cards, cards)
    click.echo(f"Generated hands: {BridgeModel.hands_to_readable_hands(hands)}")
    bridge_model = BridgeModel(cards, cards, {'board': [-1, -1, -1, -1], 'lefts': [0, 0],
                                              'hands': hands, 'next': 0, 'history': [],
                                              'beginning': 0, 'clock': 0, 'suit': -1})
    verify_synchronous(bridge_model, imperfect)


@synchronous.command()
@click.option('--w1', type=int, prompt='Number of workers for the first castle', help='first castle workers')
@click.option('--w2', type=int, prompt='Number of workers for the second castle', help='second castle workers')
@click.option('--w3', type=int, prompt='Number of workers for the third castle', help='third castle workers')
@click.option('--life', default=3, type=int, prompt='Castle life', help='castle life')
@click.option('--imperfect', is_flag=True, help='imperfect information')
def castles(w1: int, w2: int, w3: int, life: int, imperfect: bool):
    click.echo(f"Castles ({w1},{w2},{w3}), life={life}")
    castle_model = CastleModel([w1, w2, w3], [life, life, life])
    verify_synchronous(castle_model, imperfect)


@verify.command()
@click.option('--filename', default="simple_voting_1v_2c", prompt="Model file name", help="Model file name")
def asynchronous(filename):
    model = GlobalModelParser().parse(f"stv/models/asynchronous/specs/generated/{filename}.txt")

    start = time.process_time()
    model.generate(reduction=False)
    end = time.process_time()

    print(f"Generation time: {end - start}, #states: {model.states_count}, #transitions: {model.transitions_count}")

    result = model.verify_approximation(True)

    print(f"Upper approximation\nTime: {result[1]}, result: {result[0]}")

    result = model.verify_approximation(False)

    print(f"Lower approximation\nTime: {result[1]}, result: {result[0]}")


@run.group()
def generate_spec():
    pass


@generate_spec.command()
@click.option('--n_ai', default=2, prompt='Number of AI agents', help='number of AI agents')
@click.option('--max_model_quality', default=2, prompt='Maximum model quality', help='maximum model quality')
def sai(n_ai, max_model_quality):
    input_filename, output_filename, config = template_parser.sai(n_ai, max_model_quality)
    path = template_parser.save_to_file(input_filename, output_filename, config)
    click.echo(f"Model spec saved to {path}")

@generate_spec.command()
@click.option('--n_ai', default=2, prompt='Number of AI agents', help='number of AI agents')
@click.option('--max_model_quality', default=2, prompt='Maximum model quality', help='maximum model quality')
@click.option('--imp', default=1, prompt='Impersonator id', help='impersonator id')
def sai_imp(n_ai, max_model_quality, imp):
    input_filename, output_filename, config = template_parser.sai_imp(n_ai, max_model_quality, imp)
    path = template_parser.save_to_file(input_filename, output_filename, config)
    click.echo(f"Model spec saved to {path}")

@generate_spec.command()
@click.option('--n_ai', default=2, prompt='Number of AI agents', help='number of AI agents')
@click.option('--max_model_quality', default=2, prompt='Maximum model quality', help='maximum model quality')
def sai_mim(n_ai, max_model_quality):
    input_filename, output_filename, config = template_parser.sai_mim(n_ai, max_model_quality)
    path = template_parser.save_to_file(input_filename, output_filename, config)
    click.echo(f"Model spec saved to {path}")


if __name__ == "__main__":
    run()