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

AW: [tlaplus] Re: Another naive try ...

Thanks, for pointing to the misuse of Append, a fatal mistake!
In general, I was too much focused on the clashes which may appear by pure delivering on the Right or on the Left and not covering the fact that the farmer can avoid an unwanted clash by taking back the clash victim if necessary!
A classical example not being able to abstract appropriately!
So long

-----Ursprüngliche Nachricht-----
Von: tla...@xxxxxxxxxxxxxxxx [mailto:tla...@xxxxxxxxxxxxxxxx] Im Auftrag von Dmitry Kuvayskiy
Gesendet: Donnerstag, 4. April 2013 16:55
An: tlaplus
Betreff: [tlaplus] Re: Another naive try ...

Your LeftShore and RightShore are sets, not sequences (and sequences are tuples). You cannot apply Append(), which takes sequences, for sets.
There are other problems in your code, for example you don't have an action "farmer crossing a river alone".

On 4 апр, 14:49, "Friedrich Vogt" <v....@xxxxxxx> wrote:
> . to solve the "Fox, goose and beans (rivercross) puzzle in TLA" (see 
> attached .tla file).
>
> Unfortunately it throws the following exception:
>
> 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 tlc2.tool.EvalException:
>
> Attempted to apply the operator overridden by the Java method
>
> public static tlc2.value.Value
> tlc2.module.Sequences.Append(tlc2.value.Value,tlc2.value.Value),
>
> but it produced the following error:
>
> Something is wrong in the IF clause! But what? Any hint?
>
> Fritz
>
>  shores2.tla
> 1KПросмотретьЗагрузить

--
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?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.