support multi-player games
Closed this issue · 2 comments
contrct_maker.Automaton is a modification of omega.symbolic.symbolic.Automaton to store multiple state machines. Arguably, it should be possible to model any component with two entities only: environment (lumping other players) and system. These correspond to the two quantifiers: universal and existential. So, a multi-player symbolic Automaton data structure would be superfluous in that respect.
Nevertheless, it turns out that, in practice, it is more convenient to store multiple state machines in dictionaries. The changes are relatively small, because Automaton.init and Automaton.action are already dicts. It is Automaton.win that should be come a dict too, and changes relevant to this.
This issue serves as a heads up to users about the forthcoming API change.
Automaton will change, though no such thing as a "multi-player game" exists. "Game" refers to quantifier alternation. As already remarked in the OP, there are only two kinds of ordinary quantifier (i.e., not branching). Any solver that reasons about ordinary quantifiers (branching quantifiers can be reduced to ordinary plus Skolem functions, but that is out of scope here) will have to do with two actions: component and environment.
The only "multi-player" aspect is how we group variables into lists. A player is a list of variables, equiv. a predicate about whether they are controllable. Each component spec results from combining differently a couple of pieces (mainly actions). This is where the OP is useful, regarding Automaton attributes keyed by more than two names.