Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] What causes the stucking?

Email Gateway (Jul 02 2022 at 14:21):

From: Li Yongjian <lyj238@gmail.com>
Dear expert:
In the test.thy, Isablle stuck in line 1119.
I think that simplifying the
absTransfRule (env N) M (NI_Remote_GetX_PutX_Home_ref N dst) causes the
stucking.

In fact, when the rule r is small, absTransfRule (env N) r terminates.

But when guard of r is a big formula with conjunctions of hundreds of
conjuntals,
then simplifying absTransfRule (env N) r does not terminate (or Isabelle
stuck here).

absTransfRule (env N) r calls absTranfForm (env N) (guard r).

What does the simplifying procedure do? What causes the stucking?

thanks

regards
test.thy
ECMP.thy

Last updated: Jan 04 2025 at 20:18 UTC