Re: [tlaplus] sets

[Stephan Merz <stepha...@xxxxxxxxx>]

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>