clock Ctrl_y0, S2_z, default_z; int[0,2] S1_IntStat; // Internal status of S1 int[0,2] S2_IntStat; // Internal status of S2 int[0,4] Ctrl_IntStat; // Internal status of Ctrl int[0,1] Ctrl_grant1; /// grant : S1 : INPUT : bool : false : 0=false, 1=true; /// grant1 : Ctrl : OUTPUT : bool : false : 0=false, 1=true; int[0,1] Ctrl_grant2; /// grant : S2 : INPUT : bool : false : 0=false, 1=true; /// grant2 : Ctrl : OUTPUT : bool : false : 0=false, 1=true; int[0,1] polled_S2_grant; // polled value of grant int[0,1] S1_Safe; /// Safe1 : Ctrl : INPUT : bool : false : 0=false, 1=true; /// Safe : S1 : OUTPUT : bool : false : 0=false, 1=true; int[0,1] S2_Safe; /// Safe2 : Ctrl : INPUT : bool : false : 0=false, 1=true; /// Safe : S2 : OUTPUT : bool : false : 0=false, 1=true; int[0,1] polled_Ctrl_Safe2; // polled value of Safe2 int[0,1] update_S2_Safe; // value of Safe for update int[0,1] update_S1_Safe; // value of Safe for update int[0,1] update_Ctrl_grant2; // value of grant2 for update int[0,1] update_Ctrl_grant1; // value of grant1 for update chan channel_S2_S2, channel_default_S1, channel_default_Ctrl; // // Die Kanaele fuer die Testautomaten // chan S1_Safe_0_SYNC, S1_Safe_1_SYNC, S2_Safe_0_SYNC, S2_Safe_1_SYNC, PLC_SYNC; // // Die Uhren fuer die Testautomaten // clock S1_Safe_A2_ARROWCLOCK, S1_Safe_PHASECLOCK, S2_Safe_PHASECLOCK; // // Die Flags fuer die Testautomaten // int[0,1] S1_Safe_A2_CLOCKFLAG, S1_Safe_BADFLAG; //: system S1,S2,Ctrl,PLC_S2,PLC_default; //// TRIGGER_LIST ; /// Safe1 : Ctrl TRIGGERED_BY Safe : S1 ; /// Safe2 : Ctrl TRIGGERED_BY Safe : S2 ; /// request : S1 TRIGGERED_BY_PORT Root_req1 ; /// grant : S2 TRIGGERED_BY grant2 : Ctrl ; /// request : S2 TRIGGERED_BY_PORT Root_req2 ; /// grant : S1 TRIGGERED_BY grant1 : Ctrl ; process S1 () { state /// I_am_safe:S1; clocks 0 {} I_am_safe, /// I_am_unsafe:S1; clocks 0 {} I_am_unsafe; init I_am_safe; trans I_am_safe -> I_am_safe { guard S1_IntStat==0 && update_Ctrl_grant1==0 && S1_Safe==1;/// no no -1; sync channel_default_S1!; assign S1_IntStat=1; }, -> I_am_safe { guard S1_IntStat==0 && update_Ctrl_grant1==1 && S1_Safe==1;/// no no -1; sync channel_default_S1!; assign S1_IntStat=1; }, -> I_am_safe { guard S1_IntStat==0 && update_Ctrl_grant1==1 && S1_Safe==1;/// S1 I_am_safe 1; sync channel_default_S1!; assign update_S1_Safe=0, S1_IntStat=2; }, -> I_am_safe { guard S1_IntStat==1; sync channel_default_S1!; assign S1_IntStat=0; }, -> I_am_unsafe { guard S1_IntStat==2; sync channel_default_S1!; assign S1_IntStat=0; }, I_am_unsafe -> I_am_unsafe { guard S1_IntStat==0 && S1_Safe==0;/// S1 I_am_unsafe 1; sync channel_default_S1!; assign update_S1_Safe=1, S1_IntStat=1; }, -> I_am_unsafe { guard S1_IntStat==0 && S1_Safe==0;/// no no -1; sync channel_default_S1!; assign S1_IntStat=2; }, -> I_am_safe { guard S1_IntStat==1; sync channel_default_S1!; assign S1_IntStat=0; }, -> I_am_unsafe { guard S1_IntStat==2; sync channel_default_S1!; assign S1_IntStat=0; }; } process PLC_S2 () { state starting { S2_z <= 0 }, polling { S2_z <= 1002 }, testing { S2_z <= 1002 }, updating { S2_z <= 1002 }, executing_S2 { S2_z <= 1002 }, resetting_S2 { S2_z <= 0 }; commit executing_S2, resetting_S2; init starting; trans starting -> polling { sync PLC_SYNC!; assign update_S2_Safe=1, S2_Safe=1, S2_IntStat=0; }, polling -> testing { guard S2_z>0; sync PLC_SYNC!; assign polled_S2_grant=Ctrl_grant2; }, testing -> executing_S2 { sync PLC_SYNC!;}, executing_S2 -> updating { sync channel_S2_S2?;}, updating -> resetting_S2 { sync PLC_SYNC!; assign S2_z=0, S2_Safe=update_S2_Safe; }, resetting_S2 -> polling { sync channel_S2_S2?;}; } process S2 () { state /// I_am_safe:S2; clocks 0 {} I_am_safe, /// I_am_unsafe:S2; clocks 0 {} I_am_unsafe; init I_am_safe; trans I_am_safe -> I_am_safe { guard S2_IntStat==0 && polled_S2_grant==0 && S2_Safe==1;/// no no -1; sync channel_S2_S2!; assign S2_IntStat=1; }, -> I_am_safe { guard S2_IntStat==0 && polled_S2_grant==1 && S2_Safe==1;/// no no -1; sync channel_S2_S2!; assign S2_IntStat=1; }, -> I_am_safe { guard S2_IntStat==0 && polled_S2_grant==1 && S2_Safe==1;/// S2 I_am_safe 1; sync channel_S2_S2!; assign update_S2_Safe=0, S2_IntStat=2; }, -> I_am_safe { guard S2_IntStat==1; sync channel_S2_S2!; assign S2_IntStat=0; }, -> I_am_unsafe { guard S2_IntStat==2; sync channel_S2_S2!; assign S2_IntStat=0; }, I_am_unsafe -> I_am_unsafe { guard S2_IntStat==0 && S2_Safe==0;/// S2 I_am_unsafe 1; sync channel_S2_S2!; assign update_S2_Safe=1, S2_IntStat=1; }, -> I_am_unsafe { guard S2_IntStat==0 && S2_Safe==0;/// no no -1; sync channel_S2_S2!; assign S2_IntStat=2; }, -> I_am_safe { guard S2_IntStat==1; sync channel_S2_S2!; assign S2_IntStat=0; }, -> I_am_unsafe { guard S2_IntStat==2; sync channel_S2_S2!; assign S2_IntStat=0; }; } process Ctrl () { state /// wait_for_s2:Ctrl; clocks 1 {2001} wait_for_s2, /// g1:Ctrl; clocks 1 {2001} g1, /// wait_for_s1:Ctrl; clocks 1 {2001} wait_for_s1, /// g2:Ctrl; clocks 1 {2001} g2; init wait_for_s2; trans wait_for_s2 -> wait_for_s2 { guard Ctrl_IntStat==0 && polled_Ctrl_Safe2==0 && Ctrl_grant1==0;/// no no -1; sync channel_default_Ctrl!; assign Ctrl_IntStat=1; }, -> wait_for_s2 { guard Ctrl_IntStat==0 && polled_Ctrl_Safe2==1 && Ctrl_grant1==0 && Ctrl_y0<2001;/// no no -1; sync channel_default_Ctrl!; assign Ctrl_IntStat=1; }, -> wait_for_s2 { guard Ctrl_IntStat==0 && polled_Ctrl_Safe2==1 && Ctrl_grant1==0 && Ctrl_y0>=2001;/// Ctrl wait_for_s2 1; sync channel_default_Ctrl!; assign update_Ctrl_grant1=1, Ctrl_IntStat=2; }, -> wait_for_s2 { guard Ctrl_IntStat==1; sync channel_default_Ctrl!; assign Ctrl_IntStat=0; }, -> g1 { guard Ctrl_IntStat==2; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, -> wait_for_s1 { guard Ctrl_IntStat==3; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, -> g2 { guard Ctrl_IntStat==4; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, g1 -> g1 { guard Ctrl_IntStat==0 && update_S1_Safe==0 && Ctrl_grant1==1;/// Ctrl g1 1; sync channel_default_Ctrl!; assign update_Ctrl_grant1=0, Ctrl_IntStat=3; }, -> g1 { guard Ctrl_IntStat==0 && update_S1_Safe==1 && Ctrl_grant1==1 && Ctrl_y0<2001;/// no no -1; sync channel_default_Ctrl!; assign Ctrl_IntStat=2; }, -> g1 { guard Ctrl_IntStat==0 && update_S1_Safe==1 && Ctrl_grant1==1 && Ctrl_y0>=2001;/// Ctrl g1 1; sync channel_default_Ctrl!; assign update_Ctrl_grant1=0, Ctrl_IntStat=3; }, -> wait_for_s2 { guard Ctrl_IntStat==1; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, -> g1 { guard Ctrl_IntStat==2; sync channel_default_Ctrl!; assign Ctrl_IntStat=0; }, -> wait_for_s1 { guard Ctrl_IntStat==3; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, -> g2 { guard Ctrl_IntStat==4; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, wait_for_s1 -> wait_for_s1 { guard Ctrl_IntStat==0 && update_S1_Safe==0 && Ctrl_grant2==0;/// no no -1; sync channel_default_Ctrl!; assign Ctrl_IntStat=3; }, -> wait_for_s1 { guard Ctrl_IntStat==0 && update_S1_Safe==1 && Ctrl_grant2==0 && Ctrl_y0<2001;/// no no -1; sync channel_default_Ctrl!; assign Ctrl_IntStat=3; }, -> wait_for_s1 { guard Ctrl_IntStat==0 && update_S1_Safe==1 && Ctrl_grant2==0 && Ctrl_y0>=2001;/// Ctrl wait_for_s1 1; sync channel_default_Ctrl!; assign update_Ctrl_grant2=1, Ctrl_IntStat=4; }, -> wait_for_s2 { guard Ctrl_IntStat==1; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, -> g1 { guard Ctrl_IntStat==2; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, -> wait_for_s1 { guard Ctrl_IntStat==3; sync channel_default_Ctrl!; assign Ctrl_IntStat=0; }, -> g2 { guard Ctrl_IntStat==4; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, g2 -> g2 { guard Ctrl_IntStat==0 && polled_Ctrl_Safe2==0 && Ctrl_grant2==1;/// Ctrl g2 1; sync channel_default_Ctrl!; assign update_Ctrl_grant2=0, Ctrl_IntStat=1; }, -> g2 { guard Ctrl_IntStat==0 && polled_Ctrl_Safe2==1 && Ctrl_grant2==1 && Ctrl_y0<2001;/// no no -1; sync channel_default_Ctrl!; assign Ctrl_IntStat=4; }, -> g2 { guard Ctrl_IntStat==0 && polled_Ctrl_Safe2==1 && Ctrl_grant2==1 && Ctrl_y0>=2001;/// Ctrl g2 1; sync channel_default_Ctrl!; assign update_Ctrl_grant2=0, Ctrl_IntStat=1; }, -> wait_for_s2 { guard Ctrl_IntStat==1; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, -> g1 { guard Ctrl_IntStat==2; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, -> wait_for_s1 { guard Ctrl_IntStat==3; sync channel_default_Ctrl!; assign Ctrl_y0=0, Ctrl_IntStat=0; }, -> g2 { guard Ctrl_IntStat==4; sync channel_default_Ctrl!; assign Ctrl_IntStat=0; }; } process PLC_default () { state starting { default_z <= 0 }, polling { default_z <= 1000 }, testing { default_z <= 1000 }, updating { default_z <= 1000 }, executing_S1 { default_z <= 1000 }, resetting_S1 { default_z <= 0 }, executing_Ctrl { default_z <= 1000 }, resetting_Ctrl { default_z <= 0 }; commit executing_S1, resetting_S1, executing_Ctrl, resetting_Ctrl; init starting; trans starting -> polling { sync PLC_SYNC!; assign update_Ctrl_grant2=0, update_Ctrl_grant1=0, update_S1_Safe=1, Ctrl_grant2=0, Ctrl_grant1=0, S1_Safe=1, S1_IntStat=0, Ctrl_IntStat=0; }, polling -> testing { guard default_z>0; sync PLC_SYNC!; assign polled_Ctrl_Safe2=S2_Safe; }, testing -> executing_S1 { sync PLC_SYNC!;}, executing_S1 -> executing_Ctrl { sync channel_default_S1?;}, executing_Ctrl -> updating { sync channel_default_Ctrl?;}, updating -> resetting_S1 { sync PLC_SYNC!; assign default_z=0, S1_Safe=update_S1_Safe, Ctrl_grant1=update_Ctrl_grant1, Ctrl_grant2=update_Ctrl_grant2; }, resetting_S1 -> resetting_Ctrl { sync channel_default_S1?;}, resetting_Ctrl -> polling { sync channel_default_Ctrl?;}; } //************* // //Der Demultiplexer fuer die Observablen: S1_Safe, S2_Safe, // // //*************** process TA_DEMULTIPLEXER () { state TA_DM_1, S1_Safe_SD_SYNC_NODE, S2_Safe_SD_SYNC_NODE; commit S1_Safe_SD_SYNC_NODE, S2_Safe_SD_SYNC_NODE; init TA_DM_1; trans TA_DM_1 -> S1_Safe_SD_SYNC_NODE { sync PLC_SYNC?; }, S1_Safe_SD_SYNC_NODE -> S2_Safe_SD_SYNC_NODE { guard S1_Safe==0; sync S1_Safe_0_SYNC!; }, -> S2_Safe_SD_SYNC_NODE { guard S1_Safe==1; sync S1_Safe_1_SYNC!; }, S2_Safe_SD_SYNC_NODE -> TA_DM_1 { guard S2_Safe==0; sync S2_Safe_0_SYNC!; }, -> TA_DM_1 { guard S2_Safe==1; sync S2_Safe_1_SYNC!; }; } //************* process S1_Safe_Testautomat () { state S1_Safe_WAIT_1, S1_Safe_A2_A, S1_Safe_A3_A, S1_Safe_A0_A, S1_Safe_A1_A, S1_Safe_A1_B; init S1_Safe_A0_A; trans S1_Safe_A0_A -> S1_Safe_A0_A { sync S1_Safe_0_SYNC?; }, -> S1_Safe_A0_A { sync S1_Safe_1_SYNC?; }, -> S1_Safe_A1_B { sync S1_Safe_0_SYNC?; }, S1_Safe_A1_A -> S1_Safe_A1_A { sync S1_Safe_0_SYNC?; }, -> S1_Safe_WAIT_1 { guard S1_Safe_PHASECLOCK > 0; sync S1_Safe_1_SYNC?; assign S1_Safe_PHASECLOCK = 0, S1_Safe_A2_ARROWCLOCK = 0, S1_Safe_A2_CLOCKFLAG = 1; }, -> S1_Safe_A1_A { guard S1_Safe_PHASECLOCK > 0 && S1_Safe_BADFLAG == 0; assign S1_Safe_PHASECLOCK = 0, S1_Safe_A2_ARROWCLOCK = 0, S1_Safe_A2_CLOCKFLAG = 1, S1_Safe_BADFLAG = 1; }, -> S1_Safe_WAIT_1 { guard S1_Safe_BADFLAG == 1 && S1_Safe_A2_ARROWCLOCK > 0; }, S1_Safe_A2_A -> S1_Safe_A3_A { guard S1_Safe_PHASECLOCK > 0; sync S1_Safe_0_SYNC?; }, -> S1_Safe_A3_A { guard S1_Safe_PHASECLOCK > 0; sync S1_Safe_1_SYNC?; }, S1_Safe_WAIT_1 -> S1_Safe_WAIT_1 { sync S1_Safe_0_SYNC?; }, -> S1_Safe_WAIT_1 { sync S1_Safe_1_SYNC?; }, S1_Safe_A3_A -> S1_Safe_A3_A { sync S1_Safe_0_SYNC?; }, -> S1_Safe_A3_A { sync S1_Safe_1_SYNC?; }, S1_Safe_A1_B -> S1_Safe_A1_B { sync S1_Safe_0_SYNC?; }, -> S1_Safe_A1_A { assign S1_Safe_PHASECLOCK = 0; }; } //************* process S2_Safe_Testautomat () { state S2_Safe_A4_A, S2_Safe_A5_A, S2_Safe_A5_B, S2_Safe_A6_A; init S2_Safe_A4_A; trans S2_Safe_A4_A -> S2_Safe_A4_A { sync S2_Safe_0_SYNC?; }, -> S2_Safe_A4_A { sync S2_Safe_1_SYNC?; }, -> S2_Safe_A5_B { sync S2_Safe_0_SYNC?; }, S2_Safe_A5_A -> S2_Safe_A5_A { sync S2_Safe_0_SYNC?; }, -> S2_Safe_A6_A { guard S2_Safe_PHASECLOCK > 0 && S1_Safe_A2_CLOCKFLAG == 1 && S1_Safe_A2_ARROWCLOCK >= 0 && S1_Safe_A2_ARROWCLOCK <= 0; sync S2_Safe_0_SYNC?; assign S2_Safe_PHASECLOCK = 0; }, -> S2_Safe_A6_A { guard S2_Safe_PHASECLOCK > 0 && S1_Safe_A2_CLOCKFLAG == 1 && S1_Safe_A2_ARROWCLOCK >= 0 && S1_Safe_A2_ARROWCLOCK <= 0; sync S2_Safe_1_SYNC?; assign S2_Safe_PHASECLOCK = 0; }, -> S2_Safe_A6_A { guard S2_Safe_PHASECLOCK > 0 && S1_Safe_A2_CLOCKFLAG == 1 && S1_Safe_A2_ARROWCLOCK >= 0 && S1_Safe_A2_ARROWCLOCK <= 0; assign S2_Safe_PHASECLOCK = 0; }, S2_Safe_A6_A -> S2_Safe_A6_A { sync S2_Safe_0_SYNC?; }, -> S2_Safe_A6_A { sync S2_Safe_1_SYNC?; }, S2_Safe_A5_B -> S2_Safe_A5_B { sync S2_Safe_0_SYNC?; }, -> S2_Safe_A5_A { assign S2_Safe_PHASECLOCK = 0; }; } system TA_DEMULTIPLEXER, S1_Safe_Testautomat, S2_Safe_Testautomat, S1,S2,Ctrl,PLC_S2,PLC_default;