Inconsistent action order in generated trace files

[jonathan-laurent]

Update: I merged the temporary fix #657 but I am leaving this issue open since trace generation should be fixed ultimately.

I encountered an error in Replay.ml where the Edges module throws an exception as it is asked to create an agent with an id that already exists. After some investigation, I've figured out that the reason for this is that it is currently possible for KaSim to generate trace files where within a given step, action Create agent A.8 precedes Remove agent B.8 in event.actions. In other words, the action that generates an agent with some ID comes before the removal action that makes this ID available.

In #657, I proposed a quick fix in this PR where Replay always executes removal actions before the others. It passes the TQL test suite but I am not convinced it is rigorously sound. In particular, for it to be sound, we would need the following invariants:

• No step can create and remove the same agent
• If a step removes an agent, this agent cannot be mentioned in any other action from this step

I cannot think of a counterexample easily but I may be wrong here.

More generally though, this fix I proposed is just a band-aid and the trace format should guarantee that actions can always be replayed in order. I wouldn't be surprised if KaStor ended up suffering from subtle bugs because of this too.

Model triggering the problem

This model triggers the problem when simulated with seed 0. The rule that fails to replay is the following:

%agent: S()

'r' S()+, S()- @ 1

%init: 1 S()
%mod: [E] > 1 do $STOP ;

Here is the generated trace, showing the rule name and the sequence of actions for each step:

{
  "0": [ "_init_", "new(S.0)" ],
  "1": [ "r", "new(S.0) del(S.0)" ],
  "2": [ "r", "new(S.0) del(S.0)" ]
}

As you can see, executing actions in order leads to attempting to create an agent S.0 when it alredy exists in the mixture. Also, the identifier S.0 refers to two distinct agents within a single trace step.

[feret]

The semantics of concrete actions seems to be the following one.

• When an agent is removed, no other action is stored about it (including bond releasing).
• Created agents are created without default binding/internal states.
• Bonds are inserted thanks to two symmetric actions (Bind_to ...)

To satisfy these constraints, in the module Instantiation, actions are reordered the following way:

1. Remove actions
2. Creation actions
3. Anything else.

[feret]

Note that the instantiation.subst_map2_agent_in_action allow to reindex agents in action list in a sound way without relying on their order. It applies two different substitutions according to whether the agent is in a remove action, or not.
(The desambiquisation primitive a KaStor was relying on Instantiation.subst_map2_agent_in_action).

[feret]

@jonathan-laurent, please check that this is OK for you before I can merge the branch.

[jonathan-laurent]

This is the assumption I ended up making for the trace query language too. Thanks for confirming!

Ultimately though, I think traces must be generated that respect these invariants without the need for users to do any explicit sorting. Otherwise, it is going to be too easy for people to shoot themselves in the foot.

Regarding renaming, I agree about soundness, although I cannot help but find the current status quo unsatisfactory. Implementing simple transformations such as assigning unique agent ids is really tricky right now. I think we should either make sure that such transformations are easy to implement and get right or provide all relevant utilities in a central place, with proper documentation.

More generally, I think the trace format should evolve into a straightforward, standardized format that can be easily parsed and processed by various tools, as is already the case of the snapshot format. This goes beyond the scope of this issue though. In the short term, I would simply add some documentation and merge the proposed fix.

[feret]

To my opinion, the trace format where side-free actions are self-content and atomic is much more appropriate.
(In particular, it requires an action for each bond that is removed explicitly in the rule, even if it occurs in an agent that is degraded).

In case of id conflict, doing

1. bond removal
2. agent degradation
3. agent creation (with all site implicitly free and internal state to the first value)
4. binding and internal state modification.

Seems to be the most appropriate to me and is consistent with the description of the operational semantics in the literature.
The main advantage, is that each action can be interpreted independently (the result of each action is a valid state).