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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Mon, 3 Mar 2014 09:59:12 +0100*References*: <7a410c49-33a5-48e0-b870-8575170be40d@googlegroups.com>

Hello, the line that TLC's error message points to reads S' = (( S \ {y} ) \/ {y - x}) which comes from the assignment S := ( S \ {y} ) \/ {y - x} in the PlusCal algorithm. TLC's error message is therefore actually helpful (which is not always the case): you are instructing it to compute a disjunction whose first argument is a set. Sure enough, looking at the hyperbook I see that the algorithm has to compute the union of the two sets, written in ASCII as S := ( S \ {y} ) \cup {y - x} This will fix your problem. Regards, Stephan On 03 Mar 2014, at 02:35, Gideon Yuval <gy94...@xxxxxxxxx> wrote: > I copied the set-GCD code from the hyperbook (TLA file enclosed); model-checker keeps saying > > TLC threw an unexpected exception. > This was probably caused by an error in the spec or model. > See the User Output or TLC Console for clues to what happened. > The exception was a java.lang.RuntimeException: Attempted to evaluate an expression of form P \/ Q when P was > a set of the form {e1, ... ,eN}. > line 31, col 34 to line 31, col 55 of module eucset > The error occurred when TLC was evaluating the nested > expressions at the following positions: > 0. Line 27, column 13 to line 27, column 24 in eucset > 1. Line 28, column 13 to line 34, column 29 in eucset > 2. Line 29, column 24 to line 31, column 56 in eucset > ------------------------------------------------- > S has its value {6, 15, 27} from the model > > Is there a simple fix? > > Thanks > > > > > -- > You received this message because you are subscribed to the Google Groups "tlaplus" group. > To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx. > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. > Visit this group at http://groups.google.com/group/tlaplus. > For more options, visit https://groups.google.com/groups/opt_out. > <eucset.tla>

**References**:**sets***From:*Gideon Yuval

- Prev by Date:
**sets** - Next by Date:
**temporal properties** - Previous by thread:
**sets** - Next by thread:
**temporal properties** - Index(es):