//------------Box + Technician System -------------//

//blank token
typedef struct {} black_token;
// typedef unsigned (0) black_token;
black_token black_token = <black_token;

typedef unsigned (0..7) token;


//places
place stub_monitor (0..1) black_token : black_token;
place healthy_boxes (0..#token) token : token tok : tok;
place healthy_boxes_1 (0..#token) token: token tok : tok;
place inspector_ctrl (0..1) token : 0;
place inspector_ctrl_1 (1) token : 0;
place box_ctrl (#token) token: token tok : tok;
place box_ctrl_1 (#token) token: token tok : tok; 
place faulty_boxes (0..#token) token;
place faulty_boxes_1 (0..#token) token;

//transitions
trans fix_
in { stub_monitor: black_token; inspector_ctrl: x; faulty_boxes: x; }
//out { inspector_ctrl: +x; healthy_boxes: x; }
weakly_fair true
;

trans skip_healthy
in { inspector_ctrl: x; healthy_boxes: x; }
out { healthy_boxes: x; inspector_ctrl: +x; }
weakly_fair true
;

trans normal_ex
in { box_ctrl: x; }
out { box_ctrl: x; }
;

trans fault
in { box_ctrl: x; healthy_boxes: x; }
out { box_ctrl: x; faulty_boxes: x;}
;

trans fault_
in { box_ctrl: x; faulty_boxes: x; }
out { box_ctrl: x; faulty_boxes: x; }
;

trans fix
in { inspector_ctrl: x; faulty_boxes: x; inspector_ctrl_1: y; faulty_boxes_1: y; }
out { healthy_boxes: x; inspector_ctrl: +x; inspector_ctrl_1: +y; healthy_boxes_1: y; }
;

trans normal_ex_1
in { box_ctrl_1: x; }
out { box_ctrl_1: x; }
;

trans skip_healthy_1
in { inspector_ctrl_1: y; healthy_boxes_1: y; }
out { healthy_boxes_1: y; inspector_ctrl_1: +y; }
weakly_fair true
;

//[] empty equals place faulty_boxes || <> empty equals place stub_monitor;