Computations before simulation starts

[Rivers Xiao]

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?

[Markus Kuppe]

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