[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] unexpected print output

From: Y2i <yur...@xxxxxxxxx>
Date: Thu, 14 May 2015 22:28:11 -0700 (PDT)
Cc: stepha...@xxxxxxxxx
References: <4184b0f7-c2f5-451f-a52a-f938a45cd40a@googlegroups.com> <A8099D68-FE13-4F8F-8D48-3851B730532C@gmail.com> <c5783d5e-2c9b-48f8-83a1-c4538552f481@googlegroups.com> <3dd1ca34-b24b-49d1-b0f5-06cd910530b5@googlegroups.com>

Thank you everyone!

I also noticed that my earlier sample prints <"Hello"> four times if I translate with termination checking enabled and assert commented out. Is this related to extra work required to check liveness?

References:
- unexpected print output
  - From: Y2i
- Re: [tlaplus] unexpected print output
  - From: Stephan Merz
- Re: [tlaplus] unexpected print output
  - From: Leslie Lamport
- Re: [tlaplus] unexpected print output
  - From: Andrew Helwer

Prev by Date: Re: [tlaplus] unexpected print output
Next by Date: New support policy -- please respond:
Previous by thread: Re: [tlaplus] unexpected print output
Next by thread: New support policy -- please respond:
Index(es):
- Date
- Thread