//------------CommBoxTech-------------//

//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 box_ctrl (#token) token : token tok : tok;
place box_ctrl_1 (#token) token : token tok : tok;
place healthy_boxes (0..#token) token : token tok : tok;
place healthy_boxes_1 (0..#token) token : token tok : tok;
place faulty_boxes (0..#token) token;
place faulty_boxes_1 (0..#token) token;
place inspector_ctrl (0..1) token : 0;
place inspector_ctrl_1 (1) token : 0;
place unreported_boxes (0..#token) token : token tok : tok;
place unreported_boxes_1 (0..#token) token : token tok : tok;
place reported_boxes (0..#token) token;
place reported_boxes_1 (0..#token) token;


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

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

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

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

trans report
in { faulty_boxes: x; inspector_ctrl: x; unreported_boxes: x; }
out { faulty_boxes: x; inspector_ctrl: +x; reported_boxes: x; }
weakly_fair true
;

trans skip_reported
in { faulty_boxes: x; inspector_ctrl: x; reported_boxes: x; }
out { faulty_boxes: x; inspector_ctrl: +x; reported_boxes: x; }
//weakly_fair true
;

trans fix
in { stub_monitor: black_token; faulty_boxes: x; reported_boxes: x; }
weakly_fair true
;

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

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

trans report_1
in { faulty_boxes_1: y; inspector_ctrl_1: y; unreported_boxes_1: y; }
out { faulty_boxes_1: y; inspector_ctrl_1: +y; reported_boxes_1: y; }
weakly_fair true
;

trans skip_reported_1
in { faulty_boxes_1: y; inspector_ctrl_1: y; reported_boxes_1: y; }
out { faulty_boxes_1: y; inspector_ctrl_1: +y; reported_boxes_1: y; }
//weakly_fair true
;

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

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