[tlaplus] Computations before simulation starts

[Rivers Xiao <riversshallberevealed@xxxxxxxxx>]

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/e8f2f6b4-efc3-4a79-979b-ef450399112bn%40googlegroups.com.