Change confluence check algorithm to a complete algorithm

Problem

Currently, the confluence check is partial. It is based on certain patterns, and if they match all event pairs, we can conclude confluence. If there are situations that don't match the patterns, we may either not have confluence, or we don't know. For instance, we detect diamond patterns, but only of length 2, not length 3, length 4, etc.

Idea

I got inspired by the new bounded response check algorithm of #621, which is a complete check, unlike the previous finite response check. This is an attempt to get to a complete algorithm also for confluence.

The definition of confluence is: "all finite transition paths end in the same state".

Note that I added finite to the definition. The property does not consider infinite paths anymore. To find out whether there any infinite paths, just do a bounded/finite response check.

The algorithm, for confluence of X events (X being either 'controllable' or 'uncontrollable'; the 'uncontrollable' excluding input variable events):

• S = all reachable states (based on all controllable and uncontrollable transitions, and including that all input variables can change in any state to any value).
• S_1 = all states reachable from S by taking one transition for an X event.
• If S_1 is empty, then no transitions are possible for X events. So, only one sequence, the empty sequence exists. We trivially have confluence, and are done. Otherwise, continue the algorithm.
• S_{reach} = forward reachability from S_1 for all transitions with X events. This computes all states reachable from states in S by X-event sequences. It includes S_1 and is thus not empty.
• g_X = the union of the guards of all edges with X events. These are the states where at least one X event can be taken.
• S_{end} = S_{reach} and not g_X. The states reachable by X events from states in S, where no more X events can be taken. So, the possible end states of the transition paths that we are checking.
• Compute the result:
  • If S_{end} has no states, then all states in S_{reach} have enabled transitions. Since S_{reach} is not empty, this means there are reachable states, but none of them is an end of a path. All states are part of cycles, no finite transition paths exist, and confluence holds trivially.
  • If S_{end} has exactly one state, then all finite transition paths end in the same state, and confluence holds. Note that there could be infinite transition paths, but we ignore them (they are not in S_{end}), since confluence doesn't state anything about those paths.
  • If S_{end} has more than one state, then at least two transition paths end in a different state, and confluence doesn't hold. There could be infinite transition paths, but we have evidence of confluence not holding, so it is safe to ignore this.

Addresses #892