Spinroot

Harry

Member

Registered: 2012-01-18

Posts: 8

LTL formula with more than 4096 char possible?

Hello,

actually I use very long identifiers/variable-names (>200 chars) in my LTL-formula (and in my promela-code).
Now, when I load a file, in which the LTL-formula is saved, only the first 4096 characters of the LTL-formula are parsed/read.

Is it possible to use LTL-formulas with more than 4096 characters?

I know, i could replace the identifiers/variable-names with shorter ones, but that implies a lot of work for me.

Best regards,
Harry

For example, is it possible to simply extend the range in the "main.c" and "tl_main.c" without introducing errors?
"main.c":
    ...
    if (ltl_file)
    {    char formula[4096];
        add_ltl = ltl_file-2; add_ltl[1][1] = 'f';
        if (!(tl_out = fopen(*ltl_file, "r")))
        {    printf("spin: cannot open %s\n", *ltl_file);
            alldone(1);
        }
        if (!fgets(formula, 4096, tl_out))
        {    printf("spin: cannot read %s\n", *ltl_file);
        }
        fclose(tl_out);
        tl_out = stdout;
        *ltl_file = (char *) formula;
    }
    ...

"tl_main.c":
    ...
    static char    uform[4096];
    ....

I would prefer 2^16 (65536) chars for the LTL-formula. Is this possible?
Perhap you could add a global static constant to simplify such changes in the future.

Any help or advice would be really appreciated.

Last edited by Harry (2012-01-26 15:25:07)

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: LTL formula with more than 4096 char possible?

Really, variable names of 200 chars are useful...?
Can you give an example?

Harry

Member

Registered: 2012-01-18

Posts: 8

Re: LTL formula with more than 4096 char possible?

Hi,

I use a model-to-text transformation from UML-Statecharts to Promela and from text-to-model (interpretation of the counterexample as a path in the statechart).
To retain the readability and assignments of model elements (like states, transitions, variables of the statechart) I use their full-qualified-name.
This full-qualified-name is autogenerated by the UML-Tool MagicDraw and after some preparations by myself (using valid promela code characters and so on) looks like

Model_SPIN_MachineClass:Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION

Of course I could map the full-qualified-name to a much shorter one, but that would mean a lot work:
- parsing the full-qualified-names.
- replacing all identifiers used in the promela-code and the ltl-formula
- readability of promela-code / traceability between model and promela code gets lost
- interpretation of the counterexample needs parsing, replacing of the model-element-names

Consequently, for me it would be much easier, if i could change the ltl formula limit from 4096 to 65000.

Edit:
the example shows only an identifier for an UML-Statecart with two hierachies (substate in another state).
Imagin how long an identifier could be, if the are more hierachies.

Last edited by Harry (2012-01-27 10:28:56)

Harry

Member

Registered: 2012-01-18

Posts: 8

Re: LTL formula with more than 4096 char possible?

Due to the bug posted in "http://spinroot.com/fluxbb/viewtopic.php?id=738" I cannot use my self-compiled version of spin in which I incorporated longer identifiers.
Since SPIN is crucial to our current investigations, I would like to kindly ask you if you could give a try to a short-termed compilation that incorporates longer LTL-formulae.

Harry

Member

Registered: 2012-01-18

Posts: 8

Re: LTL formula with more than 4096 char possible?

Apparently there seems to be another limit at 1024 characters for LTL-Formulae that, if exceeded, results in a spin-error (*.nvr is empty).
Example below. The LTL-Formula is correct and if shortened, Spin works correctly.

Command-Line:
spin.exe -O -a -F model.pml.ltl model.pml

LTL-Formula in file model.pml.ltl:
(<>(( ((Model_SPIN_MachineClass:Model_SPIN_MachineClass_SPIN_f_V==true) && (Model_SPIN_MachineClass:Model_SPIN_MachineClass_SPIN_f_W==true) && (Model_SPIN_MachineClass:Model_SPIN_MachineClass_SPIN_f_S==false) ) ) && (Model_SPIN_MachineClass:Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION ==16))) && (<>((Model_SPIN_MachineClass:Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION ==14))) && (<>((Model_SPIN_MachineClass:Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION ==5))) && (<>((Model_SPIN_MachineClass:Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION ==4)))

Auto-Generated-Promela-Code:

/* This file is generated by Azmun */
/* MACRO */
#define inside(var, min, max) (((var) >= min ) && ((var) <= max ))
chan Model_SPIN_MachineClass_queue = [ 0 ] of {byte}

/* INTERPRETATION
[[[ Model_SPIN_MachineClass_queue = (0) : (nil), (1) : (Model_SPIN_sendInput_SPIN_in_vib), (2) : (Model_SPIN_sendInput_SPIN_in_noVib), (3) : (Model_SPIN_sendInput_SPIN_in_manStart), (4) : (Model_SPIN_sendInput_SPIN_in_manReset), (5) : (Model_SPIN_sendInput_SPIN_in_interaction) ]]]
*/
hidden short Model_SPIN_EnvironmentClass_step = 0;
/* should be write-only and only used in ONE proctype (local) */

active proctype Model_SPIN_EnvironmentClass () {

/* INTERPRETATION
REGION _16_0_1_2240127_1327071435992_645357_330
[[[ Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE = (0) : (nil), (1) : (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_SPIN_InputGen_Signals), (2) : (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_SPIN_InitEnv) ]]]
[[[ Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION = (0) : (nil), (1) : (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_SPIN_s_b_alarmOff), (2) : (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_SPIN_s_b_alarmOn), (3) : (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_SPIN_s_v_noVib), (4) : (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_SPIN_s_v_vib), (5) : (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_SPIN_s_u_inter), (6) : (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_SPIN_InitEnvTrans) ]]]
*/
/* INITIALIZATION */
byte Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE;
Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE = 2;
byte Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION;
Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION =0;
/* NEXT-STEP CALCULATION*/
do
    :: atomic { Model_SPIN_EnvironmentClass_step++;
    /* calc next transition for ( Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION ) */
    if
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE) == 1   /* CURRENT_STATE */
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION = 1;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE) == 1   /* CURRENT_STATE */
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION = 2;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE) == 1   /* CURRENT_STATE */
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION = 3;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE) == 1   /* CURRENT_STATE */
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION = 4;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE) == 1   /* CURRENT_STATE */
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION = 5;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION = 6;
        :: else
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION =0;
    fi;
    /* calc next state for (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE) */
     d_step {
    if
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 1)
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE = 1;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 2)
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE = 1;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 3)
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE = 1;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 4)
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE = 1;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 5)
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE = 1;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 6)
        -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE = 1;
        :: else /* -> Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE = Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_SUBSTATE */ ;
    fi;
    } }
    /* calc signal put in channel Model_SPIN_MachineClass_queue due to transition-action) */
    if
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 2)
        -> Model_SPIN_MachineClass_queue! 3;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 3)
        -> Model_SPIN_MachineClass_queue! 2;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 4)
        -> Model_SPIN_MachineClass_queue! 1;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 1)
        -> Model_SPIN_MachineClass_queue! 4;
        :: (Model_SPIN_EnvironmentClass_SPIN_EnvironmentClass_SPIN__16_0_1_2240127_1327071435992_645357_330_azmun_TRANSITION == 5)
        -> Model_SPIN_MachineClass_queue! 5;
        :: else /* nothing */ ;
    fi;
    :: break;
od;
}hidden short Model_SPIN_MachineClass_step = 0;
/* should be write-only and only used in ONE proctype (local) */

active proctype Model_SPIN_MachineClass () {

/* INTERPRETATION
REGION _16_0_1_2240127_1300209442977_900105_407
[[[ Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE = (0) : (nil), (1) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471), (2) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN_InitSuper) ]]]
[[[ Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_TRANSITION = (0) : (nil), (1) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__SuperInit) ]]]

REGION _16_0_1_2240127_1300209512427_674151_473
[[[ Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = (0) : (nil), (1) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_StandBy), (2) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_AlertNReport), (3) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_Really_A_Threat), (4) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_InitMain), (5) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_Preserve_Photo), (6) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_WaitingForHelp), (7) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_WaitForInit2) ]]]
[[[ Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = (0) : (nil), (1) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T18), (2) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T19), (3) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T20), (4) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T10), (5) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T12), (6) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T05), (7) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T15), (8) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T14), (9) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T13), (10) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T02), (11) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T03), (12) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T06), (13) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T08), (14) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T09), (15) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T17), (16) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T04), (17) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_Init2Trans), (18) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T01), (19) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T07), (20) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T11), (21) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_SPIN_T16) ]]]

REGION _16_0_1_87a027a_1300798457437_945953_262
[[[ Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = (0) : (nil), (1) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_InitChain), (2) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_Feature_V), (3) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_Feature_M), (4) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_Feature_U), (5) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_Feature_C), (6) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_Feature_O), (7) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_Feature_W), (8) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_Feature_EndState), (9) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_Feature_Rules), (10) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_Feature_S) ]]]
[[[ Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = (0) : (nil), (1) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_InitChainTrans), (2) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300798796089_45253_408), (3) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300798799167_80467_412), (4) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300798802776_390975_415), (5) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300798814604_456275_424), (6) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300798988055_272257_447), (7) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300798997664_860769_450), (8) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300799001774_576813_453), (9) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300799015664_972768_462), (10) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300882053822_441939_637), (11) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300882056416_463932_639), (12) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN_ruleTransition), (13) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300883814592_32532_698), (14) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300883819388_235274_700), (15) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300883821607_862970_702), (16) : (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_SPIN__16_0_1_87a027a_1300883823545_749586_704) ]]]
*/
/* INITIALIZATION */
byte _first = 0;
bool _firstConsumed = true;
byte Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE;
Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE = 2;
byte Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_TRANSITION;
Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_TRANSITION =0;
byte Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE;
Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE =0;
byte Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION;
Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION =0;
byte Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE;
Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE =0;
byte Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION;
Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION =0;
bool Model_SPIN_MachineClass_SPIN_f_V;
bool Model_SPIN_MachineClass_SPIN_f_M;
bool Model_SPIN_MachineClass_SPIN_f_U;
bool Model_SPIN_MachineClass_SPIN_f_C;
bool Model_SPIN_MachineClass_SPIN_f_O;
bool Model_SPIN_MachineClass_SPIN_f_W;
bool Model_SPIN_MachineClass_SPIN_f_S;
bool Model_SPIN_MachineClass_SPIN_b;
short Model_SPIN_MachineClass_SPIN_t;  /* RANGE [ 0, 35 ] */
bool Model_SPIN_MachineClass_SPIN_initRdy;
Model_SPIN_MachineClass_SPIN_f_V = false;
Model_SPIN_MachineClass_SPIN_f_M = false;
Model_SPIN_MachineClass_SPIN_f_U = false;
Model_SPIN_MachineClass_SPIN_f_C = false;
Model_SPIN_MachineClass_SPIN_f_O = false;
Model_SPIN_MachineClass_SPIN_f_W = false;
Model_SPIN_MachineClass_SPIN_f_S = false;
Model_SPIN_MachineClass_SPIN_b = false;
Model_SPIN_MachineClass_SPIN_t = 0;
Model_SPIN_MachineClass_SPIN_initRdy = false;
/* NEXT-STEP CALCULATION*/
do
    ::
    if
        :: _firstConsumed == true
        ->
        if
            :: Model_SPIN_MachineClass_queue?_first
            -> _firstConsumed = false;
            :: _first = 0;
            /* Delete signal */
         fi;
        :: else;
    fi;
    atomic { Model_SPIN_MachineClass_step++;
    /* calc next transition for ( Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_TRANSITION ) */
    if
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_TRANSITION = 1;
        :: else
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_TRANSITION =0;
    fi;
    /* calc next state for (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) */
     d_step {
    if
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_TRANSITION == 1)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE = 1;
        :: else /* -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE = Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE */ ;
    fi;
    }
    /* calc next transition for ( Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION ) */
    if
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 1   /* CURRENT_STATE */
        && _first == 5   /* INVOLVED_SIGNAL */
        && ( (Model_SPIN_MachineClass_SPIN_f_U ) && (Model_SPIN_MachineClass_SPIN_f_C ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 1;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 1   /* CURRENT_STATE */
        && _first == 1   /* INVOLVED_SIGNAL */
        && ( Model_SPIN_MachineClass_SPIN_f_V ) && inside( 0, 0, 35 )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 10;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 1   /* CURRENT_STATE */
        && _first == 3   /* INVOLVED_SIGNAL */
        && ( Model_SPIN_MachineClass_SPIN_f_M ) && inside( 0, 0, 35 )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 11;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        && _first == 1   /* INVOLVED_SIGNAL */
        && ( (Model_SPIN_MachineClass_SPIN_f_V ) && (Model_SPIN_MachineClass_SPIN_t < 15) && (! Model_SPIN_MachineClass_SPIN_b ) ) && inside( Model_SPIN_MachineClass_SPIN_t + 1, 0, 35 )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 4;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        && _first == 2   /* INVOLVED_SIGNAL */
        && ( Model_SPIN_MachineClass_SPIN_f_V )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 5;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        && ( (Model_SPIN_MachineClass_SPIN_t >= 15) && (Model_SPIN_MachineClass_SPIN_f_O ) && (Model_SPIN_MachineClass_SPIN_f_C ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 7;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        && ( (Model_SPIN_MachineClass_SPIN_t >= 15) && (! Model_SPIN_MachineClass_SPIN_f_O ) && (Model_SPIN_MachineClass_SPIN_f_C ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 8;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        && ( (Model_SPIN_MachineClass_SPIN_t >= 15) && (Model_SPIN_MachineClass_SPIN_f_O ) && (! Model_SPIN_MachineClass_SPIN_f_C ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 9;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        && ( (Model_SPIN_MachineClass_SPIN_b ) && (Model_SPIN_MachineClass_SPIN_f_M ) ) && inside( 15, 0, 35 )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 20;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 3   /* CURRENT_STATE */
        && _first == 2   /* INVOLVED_SIGNAL */
        && ( Model_SPIN_MachineClass_SPIN_f_V )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 6;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 3   /* CURRENT_STATE */
        && ( (Model_SPIN_MachineClass_SPIN_b ) && (Model_SPIN_MachineClass_SPIN_f_M ) && (Model_SPIN_MachineClass_SPIN_f_S ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 12;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 3   /* CURRENT_STATE */
        && ( (Model_SPIN_MachineClass_SPIN_b ) && (Model_SPIN_MachineClass_SPIN_f_M ) && (Model_SPIN_MachineClass_SPIN_f_W ) && (! Model_SPIN_MachineClass_SPIN_f_S ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 13;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 3   /* CURRENT_STATE */
        && ( (Model_SPIN_MachineClass_SPIN_t >= 5) && (Model_SPIN_MachineClass_SPIN_f_W ) && (! Model_SPIN_MachineClass_SPIN_f_S ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 14;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 3   /* CURRENT_STATE */
        && _first == 1   /* INVOLVED_SIGNAL */
        && ( (Model_SPIN_MachineClass_SPIN_f_V ) && (Model_SPIN_MachineClass_SPIN_t < 5) && (! Model_SPIN_MachineClass_SPIN_b ) ) && inside( Model_SPIN_MachineClass_SPIN_t + 1, 0, 35 )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 16;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 3   /* CURRENT_STATE */
        && ( (Model_SPIN_MachineClass_SPIN_t >= 5) && (Model_SPIN_MachineClass_SPIN_f_S ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 19;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 4   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 17;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 5   /* CURRENT_STATE */
        && ( (! Model_SPIN_MachineClass_SPIN_f_O ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 2;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 5   /* CURRENT_STATE */
        && ( (Model_SPIN_MachineClass_SPIN_f_O ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 3;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 6   /* CURRENT_STATE */
        && _first == 4   /* INVOLVED_SIGNAL */
        && ( Model_SPIN_MachineClass_SPIN_f_M )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 15;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 6   /* CURRENT_STATE */
        && _first == 2   /* INVOLVED_SIGNAL */
        && ( Model_SPIN_MachineClass_SPIN_f_V )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 21;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) == 7   /* CURRENT_STATE */
        && ( Model_SPIN_MachineClass_SPIN_initRdy )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION = 18;
        :: else
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION =0;
    fi;
    /* calc next state for (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE) */
     d_step {
    if
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1 && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE ==0)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 4;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) != 1
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE =0;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 2)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 1;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 3)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 1;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 5)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 1;
        _firstConsumed = true   /* INVOLVED_SIGNAL_USED */ ;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 6)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 1;
        _firstConsumed = true   /* INVOLVED_SIGNAL_USED */ ;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 15)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 1;
        _firstConsumed = true   /* INVOLVED_SIGNAL_USED */ ;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 18)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 1;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 21)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 1;
        _firstConsumed = true   /* INVOLVED_SIGNAL_USED */ ;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 4)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 2;
        Model_SPIN_MachineClass_SPIN_t = Model_SPIN_MachineClass_SPIN_t + 1;
        _firstConsumed = true   /* INVOLVED_SIGNAL_USED */ ;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 12)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 2;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 13)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 2;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 14)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 2;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 19)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 2;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 20)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 2;
        Model_SPIN_MachineClass_SPIN_t = 15;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 10)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 3;
        Model_SPIN_MachineClass_SPIN_b = false;
        Model_SPIN_MachineClass_SPIN_t = 0;
        _firstConsumed = true   /* INVOLVED_SIGNAL_USED */ ;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 11)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 3;
        Model_SPIN_MachineClass_SPIN_b = true;
        Model_SPIN_MachineClass_SPIN_t = 0;
        _firstConsumed = true   /* INVOLVED_SIGNAL_USED */ ;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 16)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 3;
        Model_SPIN_MachineClass_SPIN_t = Model_SPIN_MachineClass_SPIN_t + 1;
        _firstConsumed = true   /* INVOLVED_SIGNAL_USED */ ;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 1)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 5;
        _firstConsumed = true   /* INVOLVED_SIGNAL_USED */ ;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 7)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 6;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 8)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 6;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 9)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 6;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_TRANSITION == 17)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = 7;
        :: else /* -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE = Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_2240127_1300209512427_674151_473_azmun_SUBSTATE */ ;
    fi;
    }
    /* calc next transition for ( Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION ) */
    if
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 1   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 1;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 2;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 2   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 6;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 3   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 3;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 3   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 7;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 4   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 4;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 4   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 8;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 5   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 10;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 5   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 11;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 6   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 5;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 6   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 9;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 7   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 13;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 7   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 14;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 9   /* CURRENT_STATE */
        && ( (((Model_SPIN_MachineClass_SPIN_f_S ) && (! Model_SPIN_MachineClass_SPIN_f_W ) ) || ((! Model_SPIN_MachineClass_SPIN_f_S ) && (Model_SPIN_MachineClass_SPIN_f_W ) ) ) && ((Model_SPIN_MachineClass_SPIN_f_M ) || (Model_SPIN_MachineClass_SPIN_f_V ) ) && (! (Model_SPIN_MachineClass_SPIN_f_M && (! Model_SPIN_MachineClass_SPIN_f_U ) ) ) )
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 12;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 10   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 15;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1   /* CURRENT_PARENT_STATE */
        && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) == 10   /* CURRENT_STATE */
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION = 16;
        :: else
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION =0;
    fi;
    /* calc next state for (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE) */
     d_step {
    if
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) == 1 && (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE ==0)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 1;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_azmun_SUBSTATE) != 1
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE =0;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 1)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 2;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 2)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 3;
        Model_SPIN_MachineClass_SPIN_f_V = true;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 6)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 3;
        Model_SPIN_MachineClass_SPIN_f_V = false;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 3)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 4;
        Model_SPIN_MachineClass_SPIN_f_M = true;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 7)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 4;
        Model_SPIN_MachineClass_SPIN_f_M = false;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 4)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 5;
        Model_SPIN_MachineClass_SPIN_f_U = true;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 8)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 5;
        Model_SPIN_MachineClass_SPIN_f_U = false;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 10)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 6;
        Model_SPIN_MachineClass_SPIN_f_C = true;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 11)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 6;
        Model_SPIN_MachineClass_SPIN_f_C = false;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 5)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 7;
        Model_SPIN_MachineClass_SPIN_f_O = true;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 9)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 7;
        Model_SPIN_MachineClass_SPIN_f_O = false;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 12)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 8;
        Model_SPIN_MachineClass_SPIN_initRdy = true;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 15)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 9;
        Model_SPIN_MachineClass_SPIN_f_S = true;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 16)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 9;
        Model_SPIN_MachineClass_SPIN_f_S = false;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 13)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 10;
        Model_SPIN_MachineClass_SPIN_f_W = true;
        :: (Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_TRANSITION == 14)
        -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = 10;
        Model_SPIN_MachineClass_SPIN_f_W = false;
        :: else /* -> Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE = Model_SPIN_MachineClass_SPIN_MachineBehav_SPIN__16_0_1_2240127_1300209442977_900105_407_SPIN__16_0_1_2240127_1300209512427_237118_471_SPIN__16_0_1_87a027a_1300798457437_945953_262_azmun_SUBSTATE */ ;
    fi;
    } }
    :: break;
od;
}

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: LTL formula with more than 4096 char possible?

you should indeed be able to recompile spin safely with a larger buffer size for the ltl formulae,
but yes, this could mean that you then hit another limit and you may have to change that too.
it's always safe to increase the size of internal buffers, so you can go that route.
i'm looking into the -F issue -- but can't reproduce or understand it yet....