details "cyclic" and "from formulae" contradiction

[mohit jangid]

Hi All,

When proving a lemma step by step in the interactive GUI page,  Tamarin lists the contradiction reason for branches as "cyclic" or "from formula". Is it possible to get the details about which cyclic dependency (of fact or the term) or which formula caused the contradiction on a given branch? 

Thank you

Mohit Kumar Jangid

[Jannik Dreier]

Hi,

Unfortunately Tamarin does not directly tell you which cycle or formula
caused the contradiction. But still you can get some information: in the
case of a cycle, you can inspect the graph to locate the cycle yourself.
In the case of a formula, you will find a formula "False" (or "bottom")
in the list of formulas, however this does not tell you which formula
turned false. To understand that, you can try to go one step back in
your proof (or more if necessary) and compare the formulas.

Best,
Jannik

> --
> 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
> <mailto:tamarin-prove...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tamarin-prover/86d3e5b5-0d04-4451-84df-8cb6e5a3def2n%40googlegroups.com
> <https://groups.google.com/d/msgid/tamarin-prover/86d3e5b5-0d04-4451-84df-8cb6e5a3def2n%40googlegroups.com?utm_medium=email&utm_source=footer>.

--
Jannik Dreier
Maître de Conférences | Associate Professor
Université de Lorraine | TELECOM Nancy | LORIA
rese...@jannikdreier.net | +33 3 54 95 84 46

[mohit jangid]

Thank you, Dr. Jannik, for the guidance. I am dealing with very large traces and navigating/finding the cycle, in the graph, seems difficult for now. For the formulae, I will try your tip!.