Improve identification of Type 1 consistency violation

[danilovesky]

Sometimes MPSat reports Type 1 consistency violations as Type 2 (following classification in #1176 (comment))

For example, consider this STG: inconsistent.stg.work.zip

Its consistency violation is reported as Type 2:

Error: the STG is inconsistent, signal out; its initial value cannot be assigned due to traces:
in1~, out+/2
in2~, out+, in1~, out+/2

Ideally this should be reported as Type 1:

Error: the STG is inconsistent, signal out; its rising and falling edges do not alternate in trace:
in2~, out+, in1~, out+/2

The reason for the mix up:

MPSAT checks consistency by exploring the events in the depth-first order. In this case it first finds the event corresponding to out+/2 (1st trace) and records that the initial value of out must be 0, and it stores the first trace as a proof. Then it finds the out+ event (2nd trace) and checks that it does not conflict with the initial value. Then it finds a different out+/2 event (2nd trace) in the prefix, determines that it conflicts with the initial value, and reports an error giving two traces as a proof of inconsistency.