Converting a persistent fact to a linear fact causes Tamarin precomputation to be too much

35 views

Skip to first unread message

Joshua “Sync” Singla

unread,

Aug 25, 2024, 5:48:41 AM8/25/24

to tamarin-prover

I have a persistent fact that is used in three rules. When I convert it to a linear fact, the pre-computation becomes really intensive and I can't use the interactive viewer.

When I isolate the code to just include the rules that are needed for a specific trace I want, I can use the interactive viewer. Its just when I have all my other rules (which don't directly use this fact), that cause Tamarin to essentially hang.

I am not sure how to proceed here. I would like the fact to become linear.

Daniel Clark

unread,

Aug 28, 2024, 7:05:29 PM8/28/24

to tamarin-prover

Could you provide an example model that has your issue? It'll be almost impossible to help without something to go on.