Fine-grained oracle control over proof strategy
Rob Lorch
Oracles allow the user to rank proof goals. Sometimes proof goals have multiple possible cases for how they were generated-- is there any way for the user to specify the ordering of this case analysis?
In other words-- In the following screenshot, the oracle orders the proof goals in the right pane. But, is there any way for the oracle to also order the case analysis in the left pane? Some cases for a proof goal may be more likely than others.
Thanks,
Rob
Ralf Sasse
Hi Rob,
For a successful proof all cases in the left pane must be proven
anyway, which is the historic reason why there is no option to
reorder those cases.
Unfortunately, in a case like yours, where you want an instance
for an exists-trace lemma (or equivalently when you expect an
attack) this might be helpful, but sorry, it is not supported. It
might be an interesting additional feature though.
Cheers,
Ralf
--
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/2cca70a4-d4e9-4bc3-aa72-c4202e412c25n%40googlegroups.com.