On Wed, Jul 16, 2025 at 10:20:39AM +0200, Gabriele Monaco wrote: > On Tue, 2025-07-15 at 17:23 +0200, Nam Cao wrote: > > If I understand correctly, if after 3 tries and we still fail to > > change the > > state, we will invoke the reactor and trace_error? Doesn't that cause > > a > > false positive? Because it is not a violation of the model, it is > > just a > > race making us fail to change the state. > > > > Yes, that's correct. > My rationale was that, at that point, the monitor is likely no longer > in sync, so silently ignoring the situation is not really an option. > In this case, the reaction includes an invalid current state (because > in fact we don't know what the current state is) and tools may be able > to understand that.
Can't you bring the monitor back to the init state, and start over again? I think "da_mon->monitoring = 0;" does the trick? > I know you wouldn't be able to do that in LTL.. By the way, LTL uses > multiple statuses, so this lockless approach may not really work. Let's worry about one thing at a time ;) > I don't see this situation happening often: I only ever observed 2 > events able to race, 4 happening at the same time is wild, but of > course cannot be excluded in principle for any possible monitor. > Yet, I have the feeling a monitor where this can happen is not well > designed and RV should point that out. > Do you have ideas of potential monitors where more than 3 events can > race? > > Perhaps a full blown reaction is a bit aggressive in this situation, as > the /fault/ may not be necessarily in the monitor. > We could think of a special tracepoint or just printing. > > > Same below. > > > > Also, I wouldn't use goto unless necessary. Perhaps it is better to > > put the > > code at "out_react:" and "out_success:" into the loop. But that's > > just my > > personal preference, up to you. > > That could be done if we do a whole different thing when retries run > out, instead of defaulting to out_react. > I liked to avoid excessive indentation with those goto as well but > yeah, it may not be quite necessary. Sure, as I said before, "just my personal preference, up to you." Nam
