Re: Another naive try ...

[Dmitry Kuvayskiy <dmitry.k...@xxxxxxxxx>]

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ПросмотретьЗагрузить