prefer functions as strategies, instead of transducers with internal state

[johnyf]

Functions are what is synthesized.
Functions are simple.
Functions are flat, because no state is nested inside them.
Functions are explicit, because all state is outside, visible to the user, who is responsible for the "wiring".
Functions are easy to use in simulation.
Functions are local, because they need to be called only when the corresponding player moves.

Transducers are an I/O construct, with the associated drawbacks of an I/O viewpoint (as opposed to state space).
Transducers are global: they maintain implicitly foreign state internally (environment state). This is harmful to simulation, and away from reality. In reality, that state is another part of the world.
Plugging together Mealy transducers results in an unnatural system that, in general, requires solving a (centralized) fixpoint to find the next state. This is not a distributed system. No more than one component can be designed this way, unless we are working with synchronous circuits and are prepared to synthesize both Mealy and Moore machines.

[slivingston]

Can you distill design recommendations from your opening post for us? What would be sufficient for closing the issue? Otherwise, your text might be better placed in a venue for discussion separate from the code, such as the mailing list.

Some of your comments are interesting, and I would respond and engage in discussion, but I do not think the issue tracker is appropriate.

[slivingston]

We could also try to use a different platform than the mailing list. I would recommend Discourse.

[johnyf]

Functions to represent strategies

Functions in code

The main change would be to represent the synthesized strategies as mathematical functions.
This representation can be a:

1. Python dict that maps tuples or some hashable dict-like object to a dict that assigns to controlled variables their next values (this works for enumerated strategies).
2. Python function that maps keyword arguments (that assign values to variables) to a dict that assigns to controlled variables their next values.
   Depending on whether an interleaving representation is used or not, different arguments would be given (<<x, y>> vs <<x, y, x'>> etc).
3. class with a method that works as the function of No.2, and a symbol table that defines variables known to that component (the component doesn't need to know the entire world), like tulip.spec.form.GRSpec.env_vars, .sys_vars and omega.symbolic.symbolic.Automaton.vars.

I plan to experiment with these in omega.

I do not favor classes, because a dict is simpler. However, the assignment given to the strategy dict would need to be hashable, so a frozendict or similar would need to be used, if the assignment is to be represented as a dict-like object (which I find a robust choice, as opposed to tuples with nameless elements -- there are also named tuples, but the simpler the better).

So, the method of a class may serve better this purpose. Miscellaneous benefits that come with a class are:

• define a symbol table
• use whatever representation for the action is suitable for the problem. I prefer a symbolic representation. Whatever the representation, it wouldn't change how the "reaction" method is called. How that method should be named is up to debate. Maybe "next" is sufficiently self-explanatory, and pythonic.

I don't expect the first experiment in this direction to be the final solution. But it would be a starting point to see what is more practical to use.

Interleaving or not

If noninterleaving representations are synthesized and simulated, then, in general, a turn-based game requires that players be asymmetric. For 2 players this means that player 0 should be "Moore" (read <<x, y, mem0>>, write x', mem0') and player 1 "Mealy" (read <<x, y, x', mem1>>, write y', mem1'). This would require synthesis of both kinds of functions, which may need to rewrite a synthesizer from scratch for the Moore case (because the Moore strategy cannot refer to y', and the conversion from a Mealy synthesizer may be equally convoluted). Duplication in implementation means more errors, and asymmetry of players effectively associates types with players. It would be simpler to avoid both. Handling the multiplayer case is hairy, as commented in the section below.

For these reasons, I am reluctant to work with the noninterleaving currently used in tulip. Instead, I prefer to work directly to support an interleaving representation. This can be done with an existing "Mealy" solver, as was demonstrated on branch interleaving (now deleted).

Making memory explicit

Another change implied by using mathematical functions (no magic state inside them) is that the transducer's memory will need to be explicitly defined by the synthesizer. The variables mem* serve as memory throughout this comment. Internally, this is done by all synthesizers, as far as I know. In symbolic representations, the memory is readily available as a fresh variable(s for Rabin 1). Enumerated strategies would need to somehow provide this information.

About the simplicity of functions, and the benefits of making any state visible to users (that may be students), I think that a similar argument applies as "Mathematical functions are simple; ... Pascal functions are complicated..." on p.873 of "The temporal logic of actions", with "Mealy machines" in the role of Pascal functions (both involve some state invisible to the user).

Representation with interleaving behaviors

A system can be represented in logic with interleaving or without. A behavior is interleaving if in no step any changes to variable values are attributed to more than one player. Interleaving specifications are introduced on p.137 of "Specifying systems" by Lamport.

I was writing non-interleaving specifications (common in the GR(1) literature), until the mistakes that resulted from priming nuances and asymmetry between environment and system convinced me that I should not trust specifications written in this way.

Abadi and Lamport write in "Conjoining specifications", p.515:

"We have found that, in TLA, interleaving representations are usually easier to write and to reason about. Moreover, an interleaving representation is adequate for reasoning about a system if the system is modeled at a sufficiently fine grain of atomicity."

A list of advantages that interleaving specifications enjoy (not exhaustive):

• Interleaving specifications are symmetric between environment and system.
  This allows for using the same solver to synthesize both an environment and a system implementation. Having implementations for both enables both simulation and building a system from multiple components that we design.
• Interleaving specifications are easier to read and write. It is challenging, to impossible, to write a pair of correct specifications for a Moore environment and a Mealy system that cooperate, and get all the priming correct.
• Interleaving makes compositional approaches easier to simulate and reason about.
• Interleaving accommodates as many players as we like. In contrast, to ensure that a game with non-interleaving representation is turn-based, we would have to define players of different "Mealy" degree, for example:
  • player 0 reads <<x, y, z, mem0>> and writes x', mem0'
  • player 1 reads <<x, y, z, x', mem1>> and writes y', mem1'
  • player 2 reads <<x, y, z, x', y', mem2>> and writes z', mem2'.
    I don't find this very practical for writing specifications, and would be surprised if specifications written in this style didn't take many iterations until corrected to mean what the specifier wanted.
• Implementations and simulation of interleaving specifications can be understood as what we may (informally) call "causal". No need for fixed-point semantics to find the next state of a composition of "Mealy" machines (p.136, "Introduction to embedded systems", 1st ed).
• Assumptions about turn taking that are otherwise implicit in how symbols are primed (which is subtle and not obvious if not familiar with this particular syntax) become explicit, expressed with an auxiliary scheduling variable for that purpose. I have taken this approach in this solver.
• No memory about the past comes for free. Unfortunately, memory of previous environment variables is hardcoded as x (unprimed env variables) in the usual GR(1) formulation. This leads to an inaccurate complexity analysis.

Who owns the scheduling variable ?

Finally, there is a detail worth noting that also came up in discussion: an interleaving representation may or may not be perfectly interleaving, depending on who "owns" the scheduling variable that signifies who's "moving next". If the same player controls this variable throughout, then the game is still non-interleaving. But it is non-interleaving due to only this variable (that serves as a digital clock). With respect to the rest of the variables, the representation is interleaving.

If the scheduling variable changes owner (a shared-state representation), then an interleaving representation results, which is not disjoint-state any more. I don't think that the formal definition of "interleaving" and what a single variable does should distract us from the benefits of what the rest of the variables are doing, making a specification "interleaving in essence".

[necozay]

I would prefer if interleaving is not the only option. It makes sense for "board games" or software but for anything physical, it is not reasonable to expect that you can freeze the dynamics of a system until the environment moves and vice versa. I prefer to use Moore synthesizers for hybrid problems.

[necozay]

Can you say a bit more abou how you are imagining to use functions for control strategies that require memory? I can imagine a function that takes as input all the history up to that point in time, so input is a sequence with unspecified length but this does not sound like a good idea (states make the memory rep. more compact).

[johnyf]

Having both is possible. My interest is mainly in implementing the interleaving one.

Taking the above arguments and previous discussion into account, I would expect that a noninterleaving representation would be used in simpler problems that are one-sided (not compositional, and perhaps with only a system synthesized). That case seems simpler to implement, because it doesn't need a Moore synthesizer (the winning set computation using a Moore synthesizer doesn't differ much, it is already implemented, but I expect that the strategy construction will need some existential quantification to eliminate y' from the target sublevel predicates).

For the sake of investigation and comparison, implementing both would be a prerequisite for making a comparison in practice.

[johnyf]

About the freezing of dynamics, I think that this is a matter of identifying passage of physical time with steps between consecutive states in a behavior (a sequence that models a temporal logic formula). It is an issue that needs to be discussed.

Using stutter-sensitive specifications, the usual approach is to let steps correspond to passage of physical time (in discrete jumps). But that is not necessary. Still with a stutter-sensitive specification, we can let another (agreed) number of steps correspond to physical time. In particular, in an interleaving representation, 2 time steps can be understood as 1 discrete physical time step.
Due to the scheduling variable (let that be i), both players will move, one of them in each of the logic steps.

This leaves us with deciding how the physical world is going to evolve "at the same time". There are at least two alternatives:

1. define auxiliary variables that store the choice of player 0, until player 1 moves and "copies" that choice to the physical variables, thus simulating a simultaneous change happening in the real world.
2. require that a property holds only at states that follow physical time increment (for example state s_1 in the step <<s_0, s_1>>). This can be done by writing []( (i = 1) => Invariant ).

I think that No.2 is a better choice, because it doesn't introduce any additional variables, and it minimally affects the specification. Also, it is just another way to write the existing, noninterleaving specifications, as has already been remarked in other discussion. It may seem somewhat unnatural to require that a property hold only at certain states in a behavior, but that is already the case in noninterleaving specifications. When both players move in one time step, the "middle states" do exist in the game, but don't appear in the logic. So, the information flow isn't as evident.

This can make a difference, if, together with the physical variables, there are also computing signals that do participate in intermediate states, because of their much higher frequency (see also comment below). By using an interleaving representation, we force ourselves (and students) to ask these questions, and apply invariants though all time (both i = 0 and i = 1 states in a behavior), to those signals where it is appropriate.

In relation to the quote above from Abadi and Lamport, such a specification expresses things with a finer grain of atomicity, and in so doing "magnifies" what is happening, making it easier to read and understand the information flow.

To connect with the literature, specifications like those we are discussing, where time plays a role, are called real time specifications. Disassociating logic steps from physical time accommodates also for separation of time scales (as in singular perturbation theory) and refinement.

Comment on efficiency of implementation

It should be noted that my suggestion is targeting mainly how users write specifications. Using an extra variable i, and coupling other variables to it may have adverse effects in a symbolic implementation. However, I view automated recognition of this case, and conversion to a Mealy solver that makes i implicit more as an optimization, rather as an interface to the user.
Until such a conversion proves necessary because a problem cannot be solved otherwise, a simple encoding should work.

[johnyf]

I prefer Moore players too. But a noninterleaving game with Moore players is concurrent. We can still synthesize for GR(1) properties with a Moore synthesizer. Arguably, it could also be more realistic. But what a concurrent game really is is a game with partial information. This can be emphasized more in an interleaving representation with explicit hiding. A concurrent game is not determined, meaning that if a player cannot win, then this doesn't imply that the opponent can win for the negated property as objective.

If we want to work with a turn-based game and Moore players, then I think that the representation will have to be interleaving.

The only exception is the scheduling variable, if a disjoint-state representation is desired. Then, the game is concurrent, but because the scheduling variable changes in a deterministic way (it is a history variable), it can be proved that the game is equivalent to a "Mealy" game, and thus encoded and solved with an existing solver (like gr1c etc).

Side comment: a Moore system with a Mealy environment is subject to the same issues as a Mealy system with a Moore environment, if we are interested in synthesizing both, and still require reasoning about asymmetrically primed specifications.

[johnyf]

The question of what argument is given to a function that represents a strategy is a good point, because at least two approaches are commonly encountered in the literature:

1. feed function f with h, a variable that records the entire history, up to that behavior state, of variables mentioned in the specification of f, so that []( y' = f[h] ).
2. feed function f with the current values of some variables, so that []( y' = f[<<x, y, mem>>] ).

I propose No.2, which is also what is used (informally as prose mixed with math) in the definition of GR(1) synthesis on p.915 of "Synthesis of reactive(1) designs".

I would like to point out that, as written, No.1 and No.2 are the same, because h is just another variable. The difference is in what values variable h is allowed to take. So, it is in the type invariant that we require to hold for h. Let us use mem for No.1 too, instead of h. We can then observe that:

1. mem is an infinite memory that is updated with the values of x, y, and a fresh variable that serves as transducer memory.
2. mem is a finite extra memory that was introduced as controller state. The existing variables x, y are also given directly to the function.

No.2 is realistic, because it involves the current state only, and the extra memory requirements take the form of what type invariant holds for mem ([]( mem \in SomeSet )). The SomeSet depends on what type of specification we synthesize for (GR(1), Rabin(1), GR(k), etc.).

No.2 is also what is already used, for example in gr1c. The tuple <<x, y, mem>> is the annotation of the returned strategy. For example, in strategies returned by gr1c, this annotation is given as the values associated to the keys state (a tuple for <<x, y>>) and mode (for mem).

For a Mealy player, x' need be given too, so in that case f[<<x, y, x', mem>>]. Strategies from gr1c constructed from noninterleaving specifications have an x' that matters, and is obtained by first moving the environment (using a synthesized function for the Moore player, getting a satisfying next state for the environment's action, or just using Python's random), to be fed to f.

For Moore players, f[<<x, y, mem>>].

A remark that feeding f with values outside its domain does result in some behavior, but we don't know what behavior that is (untyped logic, which reflects reality too, because the world wouldn't stop if too large a current was fed into the controller. It would burn the controller, and so its output would still be something, but who knows what. In that sense, the real world is untyped. It never stops because some type checking didn't work out). So, an Exception should probably be raised in this case.

[johnyf]

Relevant to #146.

[johnyf]

Also, it may be useful to contrast the state-space based approach using functions (and the explicit quantification of initial states that will accompany it) to how long (and confusing) the discussion was in (the otherwise very useful) #93.

[johnyf]

Also, this way of simulating things is the simplest loop that a one may write to integrate a system of differential equations. The user just needs to be told what extra variables appeared (the various memories, for tracking goals or remembering past values, e.g., because past temporal operators were used) when the strategy was synthesized. API calls can be provided for this purpose, it doesn't have to happen entirely manually.

[necozay]

No.1 above is a controller; No.2 above is a controller state update function.

Consider you have a simple not-memoryless controller of the form (could be a PID controller - btw, control is usually an upper level class, junior year so no freshmen :-))

x(t+1)= f(x(t), u(t), e(t))
y(t)=g(x(t))

What you describe in No. 2 is f here. It is not the controller. Any control implementation will need to store the state explicitly. Remembering the history as in No.1 requires infinite memory so not physically possible.

Might be easier to return f and let the person simulating (or implementing) it explicitly write down the state update. But I would recommend not calling f the controller or strategy; it is just an update function.

[johnyf]

I agree that the value of variable mem will need to be stored. The values of x and y may be sensed or stored within the controller, depending on what they are.

Returning f and having the user utilize it as needed is what I have in mind, so that the class and alternatives above are packaging of f. I'd like the packaging to be thin, but some additional information may be useful to bundle with f, for example what mem is called and what values it should take.

I agree that f and mem together constitute the controller. A consequence of unnesting things is that the user is made aware of the different parts of the controller that they should implement (for example, by adding flip-flops to store the last values of mem and maybe of x, y too).

There is a mismatch though between what is called strategy in the literature, and what the implementor would call the controller, and mean all the parts that make the controller, thus including both f and h. The CS literature uses "controller" infrequently. "Strategy" is used (I think always) to refer to f (the update function), not to mem. For example:

• on p.915 of "Synthesis of reactive(1) designs": "a strategy for the system is a partial function..."
• on p.7 of "Realizable and unrealizable specifications of reactive systems" (PDF): "A strategy is a function that tells either player what its next move should be on the basis of previous moves."

We could decide to call the update function f a "strategy", and the pair <<f, m>> (maybe with other variables too) a "controller".

I mentioned the unbounded-h case because it is quite common to encounter it in the CS literature ("a (semantic) synchronous program P" in "On the synthesis of a reactive module", and "a strategy for player i" in "Playing games with boxes and diamonds"), and it is also mentioned above as what cannot be physically implemented.

In No.2, if mem is allowed to take values from an infinite set, then the two alternatives become equivalent. So the type invariance constraint on the set of memory values is essential to make the distinction. Another comment about No.1 is that it is necessary to write an update function for h itself, which would mean that someone needs to implement that.

Interestingly, that h is unbounded doesn't mean that f utilizes all the information available within h. This can be expressed with a constraint on the f that we seek to find, requiring that f depend only on a finite subsequence of h. However, this leaves h as something imaginative, which doesn't correspond to the parts of a real implementation.

[johnyf]

By "call" I mean in terminology, not in code. We could call it Function in code, and so force the user to think about how it is being used, perhaps use it for other purposes too.

[necozay]

Re interleaving:

I think non-interleaving semantics are better suited to one of the default problems in TuLiP (given hybrid system, discrete env., spec, design a controller) so I would prefer to keep Mealy or Moore solvers as default. For me, asymmetry is fine as long as you give more power to things you do not control (i.e., environment) if you want to be "robust". In general, in hybrid problems, one might even assume the system has delayed observations (though env. is superior/smart/clairvoyant and observes everything instantaneously) and solve for a delay-tolerant controller with proper reformulation to obtain an equivalent Moore or Mealy synthesis problem. Though such reformulations can be done outside the main solver to be explicit.

I agree that symmetry makes sense when dealing with multi-agent control and distributed settings to give "equal power" to all agents involved. But still if there is anything for which one does not design a controller, it can be assumed to be superior (an environment for the multiple agents; not the "environment" for individual ones).

As for interleaving semantics, it is convenient for (i) proving things in distributed, multi-agent settings, (ii) simulating distributed, multi-agent systems. But I believe it is hard to impose interleaving when physical processes are involved so might be far from reality when physics is involved. Maybe there are proper reformulations to get other type of orderings in games even the default solver assumes interleaving but having it as default might not be the best option for hybrid systems.

[johnyf]

I have been thinking about a suggestion by @necozay to use a Moore system, but let the environment be Mealy. I still think that it would be good to have a symmetric formulation, with both players being Moore machines. After thinking about these, it seems that we can have a single solution that serves all purposes. I describe this below.

Summary

• both sys and env Moore: this is symmetric.
• env Moore doesn't matter for non-compositional work, because no one has been using a Mealy environment in tulip in this case anyway.
• env Mealy can be an option, but won't add anything.
• noninterleaving specs can still be written with the above, or interleaving ones, if so desired. In other words, if noninterleaving specs are preferred, then they can still be used.
• assuming a Moore env positively affects synthesis, i.e., it is conservative. A Mealy env is dangerous, because it allows people to ask from the environment things that it cannot do. In other words, a Mealy env allows too strong assumptions to be written. For this reason, it should be avoided.

So, we can assume a concurrent game with Moore players, and write noninterleaving or interleaving specs as desired. Since non-compositional work doesn't touch the environment, this lets noninterleaving specs be used for it. But symmetry is ensured (which turns out to be decoupled from interleaving, in this case). Determinacy is lost, but, who relied on determinacy? (see also comment below about counter-strategies as debugging aid).

Conversely, if anyone would like to specify a more complex, bidirectional interaction with the environment, then they probably want to write an interleaving spec. They can still choose to write a noninterleaving one, but most likely they'd like to work with Moore machines, since these will represent engineered components. Mealy players could be included as an option, though the previous observations seem to render them obsolete.

Details

Terminology

Before continuing, a few informal definitions / summarizing notes:

• interleaving / non-interleaving can be defined with a temporal logic formula as a property of behaviors. So, it can be considered as part of the definitions we choose, instead of the semantics. This lets it be a matter of choice, within the same logic, of what kind of synthesis one chooses to perform.
• The kind of synthesis can be defined in temporal logic, and a controller is:
  • "Moore" if we ask \E f: ... y' = f[<<x, y, mem>>]
  • "Mealy" if we ask \E f: ... y' = f[<<x, y, x', mem>>]
    assuming a disjoint-state specification (variables controlled by same players throughout time).
• Whether the system is Moore is independent from whether the environment is Moore or Mealy, and the latter determines whether we have a concurrent game or not. To obtain symmetry in the specification (which I strongly support), we would let the environment be Moore too.

Symmetry: everyone Moore is conservative, so good

The key point is that the environment being Moore is about what it can accomplish, not about how much the system can accomplish. In other words, if we give less power to the environment regarding what can be written in the assumption, then this means that we can assume less. It doesn't give less power to the opponent, because the opponent is the universal quantifier, not the assumption. The universal quantifier for the system already is pessimistic enough.

So, a "Moore" assumption doesn't make things easier for the system. It makes them more difficult. I know that this sounds counter-intuitive, but that's the case. A simple way to see this, is to think about what happens if env can see y'. If it can, then we can write an assumption that requests it to react quickly to us, and so protect us. By not writing this kind of "Mealy" assumption, we make it more difficult for the system to be helped by the environment.

Interleaving is a separate concern

This leaves interleaving / non-interleaving as a separate choice. Taking into account that well-separated environments and non-compositional problems (as is most of what tulip has been used for so far) don't need an environment that "reacts intelligently" to the system, I think that it shouldn't be a problem to let the environment be Moore.

The universal quantifier is still as powerful an adversary as a Mealy environment would be, so this does not help the system in any way. The only thing that changes is that one shouldn't refer to y' in the environment's specification.
After all, the environments used so far have been Moore, so this change shouldn't affect them (only the system side would be affected, but there seems to be agreement on preferring a Moore system).

General API

Going a step further, any game can be supported, by asking for a suitable definition to be given. The definition should contain what capabilities each player (sys, env, etc.) has, i.e., whether the player's strategy f can see primed variables of other players, or not. cf. also game structures in "Alternating-time temporal logic". This changes:

• the order of \E and \A quantification when computing controllable predecessors, and
• how the sublevel sets are quantified during strategy construction.

About the environment being Mealy: I definitely agree that it is better to be pessimistic about what env can do. But, as discussed below, this pessimism is already present due to the universal quantifier. It is better to assume that the environment, too, is Moore, because that prevents us from asking from the environment things that it cannot do. Since the specs where this matters are compositional, involve cooperation between env and sys, and will likely involve synthesizing both sides, I think that in those cases one would probably choose to keep a Moore environment, and write an interleaving spec. They could also choose a Mealy environment and write a non-interleaving spec.

In any case, supporting both interleaving and non-interleaving synthesis is a matter of definition.

Those interested in synthesizing counter-strategies as an aid to understand why synthesis failed should still synthesize a Mealy environment. But, that environment is fictitious: it is a manifestation of the workings of the universal quantifier (like a ghost), not of an engineered component.

[johnyf]

The previous is essentially about the gap between the universal quantifier, and what the environment can be assumed to be capable of. This gap is what makes a game determined or not. Rephrased, a Moore env is about what behaviors we can exclude via an assumption in our spec. It is about how much we can ask from the opponent (the universal quantifier), but not about how much the opponent can do against us (which remains unchanged).

[johnyf]

About the comment above regarding interleaving specs that represent physical processes.

Yes, physical processes can be described by interleaving specifications, equivalently to how they can be described with noninterleaving specifications. The way to achieve this is by means of an auxiliary variable that "slices" states in a behavior, selecting some of them (those at time increments). The resulting spec looks something like []( (i = 1) => Invariant ), as was remarked above.

[murrayrm]

At the risk of jumping into a conversation that I don't completely follow, one thought on the use of functions to encode controllers (really the update law): one of the reasons that this might be useful is that you could, in principle, use the current state for the memory instead of the expected state. This is roughly what happens in traditional control systems: we don't assume that the state evolves according to the model that we used for synthesis, but rather read the state (often through an estimate) and send that to the update function. Of course, the controller can also have internal state (like a dynamic compensator), which would correspond to the case were part only part of the memory is updated based on measurements.

[necozay]

Switching to a function representation seems reasonable. Couple of things:

• We should think about the initialization of the memory variable as it will affect correctness (should choose a default value maybe?)
• These update rules that synthesis tools return are usually partial functions. They are not defined for all values of their domain. We should think about how to complete it to a total function (e.g., should it return None?)
• I am not sure about the implications of the function representation on code generation. I believe JPL autocoder or Simulink requires automaton like objects for code generation but I might be wrong.

[murrayrm]

Good points. I think we definitely want to maintain the current capability to generate automata, in addition to enabling the output be in the form of a function.

[johnyf]

Details of function representation

• Memory is an interesting point to raise, because it touches upon existential temporal quantification The definition of synthesis can ask for either a fixed initial value of mem, or a set of initial conditions (clearly, the former is the special case of restricting cardinality to a singleton). In other words, an initial condition of the form mem \in M is synthesized, by asking for \E M, f: ....

  Note the importance of M being a set, as opposed to a higher-order type. In an untyped first-order logic like TLA+, we can quantify only over sets (functions, too, are sets, not to be confused with operators).

  So, it suffices to return some representation of M. I prefer an initial predicate mem \in M. If symbolically represented, omega.symbolic.symbolic.Automaton (see below) can serve as a data structure to store both Init_mem == mem \in M and f, within the attributes init and action.

  I am reluctant to jump into writing yet another class for something so simple. It is better to write the absolutely necessary functions, and structure them only to the extent needed, after using them for some time. As Alan Perlis recommends in his epigrams on programming:

  • "Functions delay binding; data structures induce binding. Moral: Structure data late in the programming process."
  • "It is better to have 100 functions operate on one data structure than 10 functions on 10 data structures."

  Unfortunately, novice Python programmers (including an earlier version of myself) tend to over-structure, disoriented by the presence of object-orientation. This symptom should be avoided. Functions are simple and flat, classes are not, unless very carefully written from usage experience.

  Picking an initial value from M is a matter of enumeration for simulation, and can be done with a suitable function call for finding satisfying assignments, much like what was discussed here. In other words, the first step of simulation (before entering any loop) should be to find an assignment that satisfies all initial conditions (Init, Init_mem, and concretize, when necessary, to inclusion within certain polytopes).

• Memory for GR(1) problems and problems specified by Init /\ [][Next]_v /\ SomeLiveness (no temporal quantifiers, i.e., deterministic) can, I think, take as initial value any value that it can take throughout execution. (For GR(1) I'm sure, for the general case it'll need some proving.) The reason is that memory in the absence of quantification should be related only to liveness, so we could "cut" at any point through execution that satisfies the initial conditions on the visible state (memory is hidden), and starting from that state with the value of memory at the step we cut would still be winning (including satisfaction of Init). So, the possible initial conditions are all of the values that mem is allowed to take.

• "Partial" functions: a lot of things can be said on this topic, but to remain focused, in an untyped logic like TLA+ there are no partial functions, in the sense that partial is meant in typed logics. f[x] means something, whatever the x. We just don't know what f[x] is, if x \notin \DOMAIN f. So, we cannot prove anything about f, meaning that an f that needs to go outside its domain doesn't solve the synthesis problem (maybe it does, but there is no way to prove it).

  Returning to the problem, the "partialness" here refers to the freedom of choosing a \DOMAIN f smaller than what values initially seem necessary, e.g., those that are allowed by the type invariants. So, this is a question about how we should represent \DOMAIN f. Strictly speaking, this is a set, so another BDD or formula (for example, the formula WinningSet) that should be stored in some form.

  Even though explicit is better than implicit, it may not be necessary for simulation purposes to store \DOMAIN f, because we already store Init (where Init => \DOMAIN f). By induction, a winning f never exits \DOMAIN f (for the reasons mentioned above), so f itself is charged with the task of remaining within \DOMAIN f.

  I like that (eventually) this points at WinningSet (which is the largest it would make sense for \DOMAIN f to be) being thrown away by all synthesizers. This is a good reason for giving WinningSet a place in the synthesized result.

  I agree that a simple and pythonic API would return None to signify that the given x \notin \DOMAIN f. Note that, theoretically, this is not f[x]. The software function g(x) = f[x] if x \in \DOMAIN f else None is not a function, but an operator, because it can take any argument x (so any set, and there is no set that contains all sets, so no domain for g).

Keeping and deleting code

I agree that the current code can stay where it is, until the replacements make it obsolete. At that point it may be better to either delete it or move it at a different place. In any case, constructing a state machine of some form, possibly annotated with quantification (in the form of liveness) should definitely remain. My preference is for symbolic representation, because it works for any problem that synthesis worked (enumerated state machines work only for small problems).

Even with the functions suggested in this feature, packaging the function together with its memory for use by others requires a suitable data structure. It may also arise for simulation purposes, like a "breadboard" where one registers and connects functions and memories.

There are also a few other points. (Semi-)enumerated and symbolic representations of state machines will remain in one form or another, because they enable representation of problem input. The semi-enumerated ones currently available are in tulip.transys (a subpackage with thousands of lines) and omega.automata (a module with 400 lines).

I support the latter in favor of the former, because it is a rewrite that drops unnecessary, ill-designed, or defunct features, uses little code (one file, fewer bugs). It doesn't contain most of the things in transys, but it serves the same tasks. This and code that I comment on below have been written by me, so I am commenting on my own code. The history here recorded what was deleted and altered to obtain those from transys. There is almost no deviation there from networkx. There are only a few conventions that are defined in the docstrings.

Likewise, the 900 hundred lines I've written in tulip.synth that convert transition systems to logic have been reduced to 300 lines in omega.symbolic.logicizer that are easier to understand and debug, and do a little bit more. The rest of synth is mostly frontend to interfaces (synth.synthesize etc) and converting game-graph-like strategies to Mealy I/O transducers, which I think are disjoint in function from the conversion. omega doesn't contain any interfaces (it has synthesizers for symbolic Streett(1) strategies and counter-strategies in omega.games.gr1 that are interfaced to from tulip.interfaces.omega), so that second part of synth has no counterpart.

On the side of logic, omega.logic was written based on the parser and AST I've written in tulip.spec. The main addition is a bitblaster that compiles integer arithmetic, and past temporal logic. The bitblaster is used in openpromela. One benefit of a bitblaster is writting arbitrary quantified first-order expressions, for example x' = y - 1 (I think only jtlv supported, and I don't think it supported quantifiers).

About symbolic representation, omega.symbolic contains symbolic automata, enumeration, fixpoints, and associated utilities and bddizers (parsing / flattening to bdd). The symbolic automaton data structure that I use for almost anything I do is omega.symbolic.symbolic.Automaton. The closest data structure in tulip is tulip.spec.form.GRSpec. omega tries to keep data structures at a minimum. (cf. Alan Perlis from above).
So, the same symbolic data structure is used to store first-order logic formulae as strings (init, action, winning conditions), their bitblasted propositional versions as strings, and the BDDs that represent them.

The API of all these changes, relatively slowly.
So, I think that on a long horizon these can be used as a replacement, like polytope is being used (though it replaces itself), with the Unix philosophy in mind "small, sharp tools".

[slivingston]

I bumped the target milestone for this issue, again, because the amount of remaining work to address this issue may be large, whereas there are other improvements on master branch that are worth releasing soon.