Hi Alsita,
Indeed, as Jan says, the screenshot shows a violation of your formula, that is, there is a Commit but no Running with the right parameters. The red shows an attack as expected, and the "Solved" is with respect to the negation of the property, meaning such a solution is an attack trace.
Best regards,
Ralf
Sent from my Android device with K-9 Mail. Please excuse my brevity. --
You received this message because you are subscribed to the Google Groups "tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/3A7421D2-398E-4AC1-BC90-7BA03CC87F12%40tuhh.de.
Dotted lines in the GUI are time point relations, meaning that somehow (probably from a lemma, where #i < #j) the tool knows that the one rule instance must happen before the other, with the dotted line going from the earlier to the later event.
Cheers,
Ralf
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/3546c947-6e6b-4bf1-b20c-c6cc5612df1dn%40googlegroups.com.