Re: [tlaplus] Computations before simulation starts

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

What is the cardinality of the set or sets that were defined as symmetric?  The error message suggests that the symmetry sets are quite large, leading to an overflow in the implementation.  Nonetheless, note that symmetry reduction does not provide any advantage when using TLC's simulation mode.

Markus

> On Apr 14, 2023, at 8:45 AM, Rivers Xiao <riversshallberevealed@xxxxxxxxx> wrote:
> 
> Hi, guys, I am currently running simulation on my spec. I get this error before the simulation even starts
> Error: Attempted to apply the operator overridden by the Java method
> public static tlc2.value.impl.Value tlc2.module.TLC.Permutations(tlc2.value.impl.Value),
> but it produced the following error:
> -2102132736
> 
> Then I changed my init state so it would lead to shorter trace and get
> Error: 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 util.WrongInvocationException
> : Attempted to construct a set with too many elements (>1000000).
> 
> Then I explicitly set maxSetSize to 2147483647. But I need to wait like an hour before the simulator reports "Computed 1 initial states..." and starts the simulation.
> 
> It seems before the simulation starts, simulator does some computations which invoke Permutations to compute sets. But I only has one possible init state and it was set by constants. Why does it take so long for simulator to run before simulation starts (even throws an error) when init state is already set?

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/F81397EE-AB9D-455C-BB6D-7E505FC9BBA5%40lemmster.de.