LEGOS-SLEEC-XT/exampleSituationalConflict.sleec at main · lesunb/LEGOS-SLEEC-XT · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
def_start

// Controlled events
event eCtrl_StartApproachNurse
event eCtrl_EndApproachNurse
event eCtrl_StartPickSample
event eCtrl_EndPickSample
event eCtrl_StartAuthentication
event eCtrl_EndAuthentication
event eCtrl_EmergencyEndAuthentication

// DeliveryInfo
measure vMon_deliveryPickupLocation: numeric

// RobotInfo
measure vCtrl_robotLocation: numeric

// Other monitorable measures
measure vMon_authorizedPersonnel: boolean

// Fluents
fluent ApproachNurse <{eCtrl_StartApproachNurse}, {eCtrl_EndApproachNurse}>
fluent PickSample <{eCtrl_StartPickSample}, {eCtrl_EndPickSample}>
fluent Authentication <{eCtrl_StartAuthentication}, {eCtrl_EndAuthentication, eCtrl_EmergencyEndAuthentication}>

def_end

rule_start

Rule3 when eCtrl_EndApproachNurse
          and ({vMon_deliveryPickupLocation} = {vCtrl_robotLocation})
          then eCtrl_StartPickSample

Rule7 when eCtrl_StartAuthentication
      and (not {vMon_authorizedPersonnel})
      then eCtrl_EmergencyEndAuthentication

Rule7_1 when eCtrl_EmergencyEndAuthentication
        then not eCtrl_StartPickSample

rule_end

// The situational conflict detected for rules 3 and 7_1 can be traced back to conflicts between goal fluents Authentication and PickSample, which contain the initiating or terminating events involved.