-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathps_sas_pacs_pas.conf
114 lines (97 loc) · 6.03 KB
/
ps_sas_pacs_pas.conf
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
settings basic_blocks_filename=basic_blocks.smv output_filename=out.smv vanishing_failures=${VANISHING_FAILURES}
add_requirements filename=${REQ_FILENAME}
# unit_group
unit_group name=PAS divisions=1 failing_division=${PAS_FAULT_DIVISION}
unit_group name=PS divisions=4 failing_division=${PS_FAULT_DIVISION}
unit_group name=SAS divisions=2 failing_division=${SAS_FAULT_DIVISION}
# input
input in=PS name=HLEG_P nusmv_type={0,50,80}
input in=PS name=HLEG_T nusmv_type={20,400}
input in=PS name=NF nusmv_type={0,180000,250000}
input in=PS name=MAN_RESET nusmv_type=boolean
input in=PS name=P_VALIDATE nusmv_type=boolean
input in=SAS name=HLEG_T_SAS nusmv_type={20,400}
input in=SAS name=MAN_TRIP nusmv_type=boolean
input in=PS name=MAN_OFF nusmv_type=boolean
input in=PS name=MAN_ON nusmv_type=boolean
input in=PS name=MAN_STOP nusmv_type=boolean
input in=PAS name=N_FLUX_NS nusmv_type={0,20,80,100,120}
input in=PAS name=RCP1_IN_OP nusmv_type=boolean
input in=PAS name=RCP2_IN_OP nusmv_type=boolean
input in=PAS name=RCP3_IN_OP nusmv_type=boolean
input in=PAS name=RCP4_IN_OP nusmv_type=boolean
# output
output in=PS name=RODS_DOWN
output in=PS name=RODS_UP
# unit
unit in=PS name=APU filename=ps_apu.smv max_delay=${MAX_DELAY_PS_APU} nusmv_module_name=PS_APU single_division_to_retain=NA nusmv_outputs=HLEG_P_Max2_OR_NF_Max2:boolean;HLEG_T_Min_AND_HLEG_P_Min:boolean
unit in=PS name=ALU filename=ps_alu.smv max_delay=${MAX_DELAY_PS_ALU} nusmv_module_name=PS_ALU single_division_to_retain=NA nusmv_outputs=RODS_DOWN:boolean;ENABLE_SAS:boolean;ENABLE_PAS:boolean
unit in=SAS name=APU filename=sas_apu.smv max_delay=${MAX_DELAY_SAS_APU} nusmv_module_name=SAS_APU single_division_to_retain=NA nusmv_outputs=RT_CRITERIA:boolean
unit in=SAS name=ALU filename=sas_alu.smv max_delay=${MAX_DELAY_SAS_ALU} nusmv_module_name=SAS_ALU single_division_to_retain=NA nusmv_outputs=RODS_DOWN:boolean;RODS_UP:boolean
unit in=PS name=PACS filename=pacs.smv max_delay=${MAX_DELAY_PACS} nusmv_module_name=PACS2 single_division_to_retain=NA nusmv_outputs=CMDOFF:boolean;CMDON:boolean
unit in=PAS name=PAS filename=pas.smv max_delay=${MAX_DELAY_PAS} nusmv_module_name=PAS single_division_to_retain=NA nusmv_outputs=RODS_UP_GROUP_1:boolean;RODS_UP_GROUP_2:boolean;RODS_DOWN_GROUP_1:boolean;RODS_DOWN_GROUP_2:boolean
symmetry group=PS unit=APU input_variable_indices=1 # determinism check
symmetry group=PS unit=ALU input_variable_indices=1,2,3,4
symmetry group=PS unit=ALU input_variable_indices=5,6,7,8
symmetry group=SAS unit=APU input_variable_indices=2,3
symmetry group=SAS unit=ALU input_variable_indices=1,2
symmetry group=SAS unit=ALU input_variable_indices=5,6
symmetry group=PAS unit=PAS input_variable_indices=1,2,3,4
symmetry group=PAS unit=PAS input_variable_indices=6,7,8,9
symmetry group=PS unit=PACS input_variable_indices=1 # determinism check
# connections to PS.APU
parallel_connection from=input.HLEG_P to=PS.APU
parallel_connection from=input.HLEG_T to=PS.APU
parallel_connection from=input.NF to=PS.APU
# connections to PS.ALU
all_to_all_connection from=PS.APU.HLEG_T_Min_AND_HLEG_P_Min to=PS.ALU
all_to_all_connection from=PS.APU.HLEG_P_Max2_OR_NF_Max2 to=PS.ALU
parallel_connection from=input.MAN_RESET to=PS.ALU
parallel_connection from=input.P_VALIDATE to=PS.ALU
# connections to SAS.APU
parallel_connection from=input.HLEG_T_SAS to=SAS.APU
single_connection from=input.NF.1 to=SAS.APU.1
single_connection from=input.NF.2 to=SAS.APU.1
single_connection from=input.NF.3 to=SAS.APU.2
single_connection from=input.NF.4 to=SAS.APU.2
# connections to SAS.ALU
all_to_all_connection from=SAS.APU.RT_CRITERIA to=SAS.ALU
parallel_connection from=input.MAN_TRIP to=SAS.ALU
single_connection from=PAS.PAS.RODS_UP_GROUP_1.1 to=SAS.ALU.2
# was originally from PAS.PAS.RODS_UP_GROUP_2, replaced to infer symmetry:
single_connection from=PAS.PAS.RODS_UP_GROUP_1.1 to=SAS.ALU.1
single_connection from=PS.ALU.ENABLE_SAS.1 to=SAS.ALU.1
single_connection from=PS.ALU.ENABLE_SAS.2 to=SAS.ALU.2
single_connection from=PS.ALU.ENABLE_SAS.3 to=SAS.ALU.1
single_connection from=PS.ALU.ENABLE_SAS.4 to=SAS.ALU.2
# connections to PACS
parallel_connection from=PS.ALU.RODS_DOWN to=PS.PACS
parallel_connection from=const.FALSE to=PS.PACS
single_connection from=SAS.ALU.RODS_DOWN.1 to=PS.PACS.1
single_connection from=SAS.ALU.RODS_DOWN.1 to=PS.PACS.3
single_connection from=SAS.ALU.RODS_DOWN.2 to=PS.PACS.2
single_connection from=SAS.ALU.RODS_DOWN.2 to=PS.PACS.4
parallel_connection from=const.FALSE to=PS.PACS
single_connection from=PAS.PAS.RODS_DOWN_GROUP_1.1 to=PS.PACS.1
single_connection from=PAS.PAS.RODS_DOWN_GROUP_1.1 to=PS.PACS.3
# was originally from PAS.PAS.RODS_UP_GROUP_2, replaced to infer symmetry:
single_connection from=PAS.PAS.RODS_DOWN_GROUP_1.1 to=PS.PACS.2
# was originally from PAS.PAS.RODS_UP_GROUP_2, replaced to infer symmetry:
single_connection from=PAS.PAS.RODS_DOWN_GROUP_1.1 to=PS.PACS.4
single_connection from=SAS.ALU.RODS_UP.1 to=PS.PACS.1
single_connection from=SAS.ALU.RODS_UP.1 to=PS.PACS.3
single_connection from=SAS.ALU.RODS_UP.2 to=PS.PACS.2
single_connection from=SAS.ALU.RODS_UP.2 to=PS.PACS.4
parallel_connection from=input.MAN_OFF to=PS.PACS
parallel_connection from=input.MAN_ON to=PS.PACS
parallel_connection from=input.MAN_STOP to=PS.PACS
# connections to PAS
all_to_all_connection from=PS.ALU.ENABLE_SAS to=PAS.PAS
parallel_connection from=input.N_FLUX_NS to=PAS.PAS
parallel_connection from=input.RCP1_IN_OP to=PAS.PAS
parallel_connection from=input.RCP2_IN_OP to=PAS.PAS
parallel_connection from=input.RCP3_IN_OP to=PAS.PAS
parallel_connection from=input.RCP4_IN_OP to=PAS.PAS
# connections to outputs
parallel_connection from=PS.PACS.CMDOFF to=output.RODS_DOWN
parallel_connection from=PS.PACS.CMDON to=output.RODS_UP