Closed johnyf closed 6 years ago
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.
Addressed in 50a1eed7bc528d0d4651eb231b73cc3f67c90082.
contrct_maker.Automaton
is a modification ofomega.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
andAutomaton.action
are alreadydict
s. It isAutomaton.win
that should be come adict
too, and changes relevant to this.This issue serves as a heads up to users about the forthcoming API change.