Skip to content

String Representation of States in mcsta Scheduler

I recently encounter a problem concerning the variable order in the states of a scheduler generated by mcsta. The position of some variables in different schedulers for the "same" model (the structure is identical, only some initial variable/array values change) vary.

Context:
I use modes to simulate a modest model according to the mcsta scheduler in order to receive the optimal trace implicitely calculated by the model checker. I currently rely on the position of the variables because otherwise I cannot distinguish between the location of all instances of the same process given that they all have the same name, e.g. Experiment.location.

In the previous model version, only the position of the global clock gc deterministically changed between the representation in the scheduler and the internal representation in modes1 / order in the output trace. This allowed for a simple fix that deterministically moved the affected entries to their correct place. This is yet not possible anymore as not even the order within the schedulers is predictable.

Example (first entry of the two schedulers):

+ State: (AttitudeControl.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Battery.location = 0, Sun.location = 0, Main.location = 0, GlobalInvariant.location = 0, GlobalSync.location = 0, a = 1, ratio = 0, AttitudeControl.a_dst = 0, gc = 0, new_time = 0, AttitudeControl.slewingEnd_time = 0, Battery.old_time = 0, ac_lock = False, slewing = False, insolation = False, Sun.updateAfterInsolationEnd = False, cost = 0, l = 134784000, sun_c = 0, Battery.r = 0, c = [0, 0, 0, 0, 0, 0, 0], nee = [0, 0, 0, 0, 0, 0, 0], pa = [False, False, False, False, False, False, False])
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |============================================================================================================================================================================================================================|
+ State: (AttitudeControl.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Battery.location = 0, Sun.location = 0, Main.location = 0, GlobalInvariant.location = 0, GlobalSync.location = 0, a = 1, ratio = 0, AttitudeControl.a_dst = 0, ac_lock = False, slewing = False, insolation = False, Sun.updateAfterInsolationEnd = False, gc = 0, cost = 0, l = 134784000, new_time = 0, sun_c = 0, AttitudeControl.slewingEnd_time = 0, Battery.r = 0, Battery.old_time = 0, c = [0, 0, 0, 0, 0, 0, 0], nee = [0, 0, 0, 0, 0, 0, 0], pa = [False, False, False, False, False, False, False])

How is the variable order in the scheduler states determined? And is it possible to keep it fixed for the same model (only with different variable assignments) or even to ensure the same order within mcsta's schedulers and modes' traces?

  1. for example the toString() of ref T currentState in Simulation/Runs/STASimulationRun.cs ↩