/*Maximal number of aplication interrupts (255=unbounded)*/
#define MAX_AP_INTS 255
/*Maximal number of LSL interrupts (255=unbounded)*/
#define MAX_LSL_INTS 255

byte cur=0;
byte sleeping=0;
byte sleep_op=0;
byte sw_stand_by=0;
byte generated_ap_interrupt=0;
byte lsl_command=0;
byte lsl_running=0;
byte lsl_data=0;
byte ap_interrupt=0;
byte enabled_lsl_interrupt=0;
byte lsl_interrupt=0;
byte lsl_interrupt_ex=0;
byte generated_lsl_interrupt=0;
byte some_running=0;
byte some_data=0;
byte some_interrupt=0;

chan ap_down =[0] of {int};
chan ap_actv =[0] of {int};
chan ap_down_ack =[0] of {int};
chan ap_down_nack =[0] of {int};
chan calc =[0] of {int};

#define AP_BOUNDED active proctype AP()\
{\
byte no_ap_ints=0;\
actv: if\
:: ap_actv?0; goto actv;\
:: atomic {no_ap_ints<MAX_AP_INTS;generated_ap_interrupt = 1;no_ap_ints = no_ap_ints+1;}  goto actv;\
:: ap_down!0; goto prepare_ack;\
fi;\
prepare_ack: if\
:: ap_down!0; goto prepare_ack;\
:: ap_down_nack?0; goto actv;\
:: ap_down_ack?0; goto stand_by;\
fi;\
stand_by: if\
:: goto actv;\
:: ap_actv?0; goto actv;\
fi;\
}

#define AP_UNBOUNDED active proctype APUnbounded()\
{\
actv: if\
:: ap_actv?0; goto actv;\
:: generated_ap_interrupt = 1; goto actv;\
:: ap_down!0; goto prepare_ack;\
fi;\
prepare_ack: if\
:: ap_down!0; goto prepare_ack;\
:: ap_down_nack?0; goto actv;\
:: ap_down_ack?0; goto stand_by;\
fi;\
stand_by: if\
:: goto actv;\
:: ap_actv?0; goto actv;\
fi;\
}

#define LSL_INTERRUPT_HANDLER active proctype LSL_Interrupt_Handler()\
{\
lsl_int_service: if\
:: atomic {cur==0 && enabled_lsl_interrupt==1 && generated_lsl_interrupt==1;cur = 1;lsl_interrupt_ex = 1;}  goto interrupt_received;\
fi;\
interrupt_received: if\
:: cur==1 && sleeping==0; goto awake;\
:: atomic {cur==1 && sleeping==1;sleeping = 0;}  goto awake;\
fi;\
awake: if\
:: atomic {cur==1;enabled_lsl_interrupt = 0;generated_lsl_interrupt = 0;lsl_interrupt = 1;lsl_interrupt_ex = 0;some_interrupt = 1;}  goto check_stand_by;\
fi;\
check_stand_by: if\
:: atomic {cur==1 && sw_stand_by==0;cur = 0;}  goto lsl_int_service;\
:: cur==1 && sw_stand_by==1; goto insert_noop;\
fi;\
insert_noop: if\
:: atomic {cur==1;sleep_op = 0;}  goto clear_stand_by;\
fi;\
clear_stand_by: if\
:: atomic {cur==1;sw_stand_by = 0;cur = 0;}  goto lsl_int_service;\
fi;\
}

#define AP_INTERRUPT_HANDLER active proctype AP_Interrupt_Handler()\
{\
byte old_cur=0;\
ap_int_service: if\
::  atomic {generated_ap_interrupt==1 && lsl_interrupt_ex==0;generated_ap_interrupt = 0;}  goto set_cur;\
fi;\
set_cur: if\
::  atomic {cur==0;old_cur = 0;cur = 2;}  goto interrupt_received;\
::  atomic {cur==1;old_cur = 1;cur = 2;}  goto interrupt_received;\
fi;\
interrupt_received: if\
:: sleeping==0; goto awake;\
:: atomic {sleeping==1;sleeping = 0;}  goto awake;\
fi;\
awake: if\
::  atomic {enabled_lsl_interrupt = 0;generated_lsl_interrupt = 0;ap_interrupt = 1;some_interrupt = 1;}  goto check_stand_by;\
fi;\
check_stand_by: if\
:: sw_stand_by==0; goto reset_cur;\
:: sw_stand_by==1; goto insert_noop;\
fi;\
reset_cur: if\
::  atomic {old_cur==0;cur = 0;}  goto ap_int_service;\
::  atomic {old_cur==1;cur = 1;}  goto ap_int_service;\
fi;\
insert_noop: if\
:: sleep_op = 0; goto clear_stand_by;\
fi;\
clear_stand_by: if\
:: sw_stand_by = 0; goto reset_cur;\
fi;\
}

#define INTERRUPT_GENERATOR_BOUNDED active proctype Interrupt_Generator()\
{\
byte no_lsl_ints=0;\
generate: if\
:: atomic {enabled_lsl_interrupt==1 && no_lsl_ints<MAX_LSL_INTS;generated_lsl_interrupt = 1;no_lsl_ints = no_lsl_ints+1;}  goto generate;\
fi;\
}

#define INTERRUPT_GENERATOR_UNBOUNDED active proctype Interrupt_Generator()\
{\
generate: if\
:: atomic {enabled_lsl_interrupt==1;generated_lsl_interrupt = 1;}  goto generate;\
fi;\
}

#define LSL_DRIVER active proctype LSL_Driver()\
{\
stand_by: if\
::  atomic {cur==0 && lsl_command==3;lsl_command = 0;}  goto stand_by;\
::  atomic {cur==0 && lsl_command==1;lsl_command = 0;}  goto up_down_received;\
::  atomic {cur==0 && lsl_command==2;lsl_command = 0;}  goto up_down_received;\
fi;\
up_down_received: if\
:: cur==0; goto react;\
fi;\
react: if\
::  atomic {cur==0;lsl_running = 0;lsl_data = 0;}  goto call;\
::  atomic {cur==0;lsl_running = 1;lsl_data = 1;some_running = 1;some_data = 1;}  goto stand_by;\
fi;\
call: if\
:: calc!0; goto stand_by;\
fi;\
}

#define CALC active proctype Calc()\
{\
idle: if\
:: calc?0; goto calc_data;\
fi;\
calc_data: if\
:: lsl_data==1; goto calc_running;\
::  atomic {lsl_data==0;some_data = 0;}  goto calc_running;\
fi;\
calc_running: if\
:: lsl_running==1; goto idle;\
::  atomic {lsl_running==0;some_running = 0;}  goto idle;\
fi;\
}

#define PROC_IOP active proctype IOP()\
{\
actv: if\
::  atomic {cur==0;ap_down?0;}  goto down_received;\
fi;\
going_down: if\
::  atomic {cur==0;lsl_data = 0;some_data = 0;lsl_running = 1;some_running = 1;}  goto clear_interrupts;\
fi;\
clear_interrupts: if\
::  atomic {cur==0;ap_interrupt = 0;lsl_interrupt = 0;some_interrupt = 0;}  goto enable_lsl_interrupt;\
fi;\
enable_lsl_interrupt: if\
::  atomic {cur==0;enabled_lsl_interrupt = 1;generated_lsl_interrupt = 0;}  goto issue_down_lsl;\
fi;\
issue_down_lsl: if\
::  atomic {cur==0;lsl_command = 2;}  goto wait_for_down;\
fi;\
wait_for_down: if\
:: cur==0 && some_running==0; goto down_expected;\
:: cur==0 && some_data==1; goto down_expected;\
fi;\
down_expected: if\
:: cur==0 && some_data==1; goto disable_lsl_interrupt;\
:: cur==0 && some_data==0; goto down_verified;\
fi;\
disable_lsl_interrupt: if\
::  atomic {cur==0;enabled_lsl_interrupt = 0;generated_lsl_interrupt = 0;}  goto issue_actv_commands;\
fi;\
down_verified: if\
:: ap_down_ack!0; goto insert_noop;\
fi;\
down_received: if\
::  goto going_down;\
fi;\
insert_noop: if\
::  atomic {cur==0;sleep_op = 1;}  goto set_stand_by;\
fi;\
set_stand_by: if\
::  atomic {cur==0;sw_stand_by = 1;}  goto check_interrupts;\
fi;\
check_interrupts: if\
:: cur==0 && some_interrupt==0; goto check_noop;\
:: cur==0 && some_interrupt==1; goto wake_up;\
fi;\
check_noop: if\
:: cur==0 && sleep_op==0; goto wake_up;\
::  atomic {cur==0 && sleep_op==1;sleeping = 1;}  goto w_stand_by;\
fi;\
w_stand_by: if\
:: cur==0; goto stand_by;\
fi;\
wake_up: if\
::  atomic {cur==0;sw_stand_by = 0;lsl_data = 0;some_data = 0;lsl_running = 1;some_running = 1;}  goto clear_int;\
fi;\
stand_by: if\
:: cur==0 && some_interrupt==1; goto wake_up;\
fi;\
clear_int: if\
::  atomic {cur==0;ap_interrupt = 0;lsl_interrupt = 0;some_interrupt = 0;}  goto issue_lsl_up;\
fi;\
issue_lsl_up: if\
::  atomic {cur==0;lsl_command = 1;}  goto wait_init_response;\
fi;\
wait_init_response: if\
:: cur==0 && some_running==0; goto data_expected;\
:: cur==0 && some_data==1; goto data_expected;\
fi;\
data_expected: if\
:: cur==0 && some_data==1; goto s_actv;\
:: cur==0 && some_data==0; goto noise;\
fi;\
noise: if\
::  atomic {cur==0;lsl_data = 0;some_data = 0;lsl_running = 1;some_running = 1;}  goto re_enable_lsl_interrupt;\
fi;\
s_actv: if\
:: ap_actv!0; goto now_wait;\
fi;\
now_wait: if\
:: cur==0; goto actv;\
fi;\
re_enable_lsl_interrupt: if\
::  atomic {cur==0;enabled_lsl_interrupt = 1;}  goto re_issue_lsl_down;\
fi;\
re_issue_lsl_down: if\
::  atomic {cur==0;lsl_command = 2;}  goto wait_response;\
fi;\
wait_response: if\
:: cur==0 && some_running==0; goto observe_status;\
:: cur==0 && some_data==1; goto observe_status;\
fi;\
observe_status: if\
:: cur==0 && some_data==0; goto insert_noop;\
:: cur==0 && some_data==1; goto clear_lsl_interrupt;\
fi;\
clear_lsl_interrupt: if\
::  atomic {cur==0;enabled_lsl_interrupt = 0;generated_lsl_interrupt = 0;}  goto send_actv_command;\
fi;\
send_actv_command: if\
::  atomic {ap_actv!0;lsl_command = 3;}  goto back_to_actv;\
fi;\
back_to_actv: if\
:: cur==0; goto actv;\
fi;\
issue_actv_commands: if\
::  atomic {cur==0;lsl_command = 3;}  goto send_nack;\
fi;\
send_nack: if\
:: ap_down_nack!0; goto enter_actv;\
fi;\
enter_actv: if\
:: cur==0; goto actv;\
fi;\
}

AP_UNBOUNDED

LSL_INTERRUPT_HANDLER

AP_INTERRUPT_HANDLER

INTERRUPT_GENERATOR_UNBOUNDED

LSL_DRIVER

CALC

PROC_IOP

never {    /* !([]((sleeping && sleep_op) -> (!(sleep_op U (!sleeping && sleep_op))))) */
T0_init:
        if
        :: ((sleep_op) && (sleeping)) -> goto T0_S4
        :: (1) -> goto T0_init
        fi;
T0_S4:
        if
        :: (! ((sleeping)) && (sleep_op)) -> goto accept_all
        :: ((sleep_op)) -> goto T0_S4
        fi;
accept_all:
        skip
}
