Skip to content

Commit

Permalink
Added material for EDCC 2020
Browse files Browse the repository at this point in the history
  • Loading branch information
volkm committed Apr 15, 2020
1 parent fecf753 commit 47559fc
Show file tree
Hide file tree
Showing 1,142 changed files with 131,228 additions and 0 deletions.
Binary file added 2020-EDCC/BDMPs.pdf
Binary file not shown.
Binary file added 2020-EDCC/EDCC-results-sheet.ods
Binary file not shown.
784 changes: 784 additions & 0 deletions 2020-EDCC/GreatSPNresults/01-result.txt

Large diffs are not rendered by default.

899 changes: 899 additions & 0 deletions 2020-EDCC/GreatSPNresults/02-result.txt

Large diffs are not rendered by default.

902 changes: 902 additions & 0 deletions 2020-EDCC/GreatSPNresults/03-result.txt

Large diffs are not rendered by default.

1,335 changes: 1,335 additions & 0 deletions 2020-EDCC/GreatSPNresults/04-result.txt

Large diffs are not rendered by default.

1,072 changes: 1,072 additions & 0 deletions 2020-EDCC/GreatSPNresults/05-result.txt

Large diffs are not rendered by default.

545 changes: 545 additions & 0 deletions 2020-EDCC/GreatSPNresults/06-result.txt

Large diffs are not rendered by default.

665 changes: 665 additions & 0 deletions 2020-EDCC/GreatSPNresults/07-result.txt

Large diffs are not rendered by default.

1,082 changes: 1,082 additions & 0 deletions 2020-EDCC/GreatSPNresults/08-result.txt

Large diffs are not rendered by default.

897 changes: 897 additions & 0 deletions 2020-EDCC/GreatSPNresults/09-result.txt

Large diffs are not rendered by default.

783 changes: 783 additions & 0 deletions 2020-EDCC/GreatSPNresults/10-result.txt

Large diffs are not rendered by default.

547 changes: 547 additions & 0 deletions 2020-EDCC/GreatSPNresults/11-result.txt

Large diffs are not rendered by default.

547 changes: 547 additions & 0 deletions 2020-EDCC/GreatSPNresults/12-result.txt

Large diffs are not rendered by default.

779 changes: 779 additions & 0 deletions 2020-EDCC/GreatSPNresults/13-result.txt

Large diffs are not rendered by default.

604 changes: 604 additions & 0 deletions 2020-EDCC/GreatSPNresults/14-result.txt

Large diffs are not rendered by default.

1,243 changes: 1,243 additions & 0 deletions 2020-EDCC/GreatSPNresults/15-result.txt

Large diffs are not rendered by default.

895 changes: 895 additions & 0 deletions 2020-EDCC/GreatSPNresults/16-result.txt

Large diffs are not rendered by default.

1,765 changes: 1,765 additions & 0 deletions 2020-EDCC/GreatSPNresults/17-result.txt

Large diffs are not rendered by default.

971 changes: 971 additions & 0 deletions 2020-EDCC/GreatSPNresults/18-result.txt

Large diffs are not rendered by default.

1,078 changes: 1,078 additions & 0 deletions 2020-EDCC/GreatSPNresults/19-result.txt

Large diffs are not rendered by default.

843 changes: 843 additions & 0 deletions 2020-EDCC/GreatSPNresults/20-result.txt

Large diffs are not rendered by default.

781 changes: 781 additions & 0 deletions 2020-EDCC/GreatSPNresults/21-result.txt

Large diffs are not rendered by default.

970 changes: 970 additions & 0 deletions 2020-EDCC/GreatSPNresults/22-result.txt

Large diffs are not rendered by default.

1,538 changes: 1,538 additions & 0 deletions 2020-EDCC/GreatSPNresults/23-result.txt

Large diffs are not rendered by default.

779 changes: 779 additions & 0 deletions 2020-EDCC/GreatSPNresults/24-result.txt

Large diffs are not rendered by default.

787 changes: 787 additions & 0 deletions 2020-EDCC/GreatSPNresults/25-result.txt

Large diffs are not rendered by default.

895 changes: 895 additions & 0 deletions 2020-EDCC/GreatSPNresults/26-result.txt

Large diffs are not rendered by default.

1,011 changes: 1,011 additions & 0 deletions 2020-EDCC/GreatSPNresults/27-result.txt

Large diffs are not rendered by default.

724 changes: 724 additions & 0 deletions 2020-EDCC/GreatSPNresults/28-result.txt

Large diffs are not rendered by default.

902 changes: 902 additions & 0 deletions 2020-EDCC/GreatSPNresults/29-result.txt

Large diffs are not rendered by default.

664 changes: 664 additions & 0 deletions 2020-EDCC/GreatSPNresults/30-result.txt

Large diffs are not rendered by default.

788 changes: 788 additions & 0 deletions 2020-EDCC/GreatSPNresults/31-result.txt

Large diffs are not rendered by default.

604 changes: 604 additions & 0 deletions 2020-EDCC/GreatSPNresults/32-result.txt

Large diffs are not rendered by default.

548 changes: 548 additions & 0 deletions 2020-EDCC/GreatSPNresults/33-result.txt

Large diffs are not rendered by default.

492 changes: 492 additions & 0 deletions 2020-EDCC/GreatSPNresults/34-result.txt

Large diffs are not rendered by default.

546 changes: 546 additions & 0 deletions 2020-EDCC/GreatSPNresults/35-result.txt

Large diffs are not rendered by default.

1,016 changes: 1,016 additions & 0 deletions 2020-EDCC/GreatSPNresults/36-result.txt

Large diffs are not rendered by default.

903 changes: 903 additions & 0 deletions 2020-EDCC/GreatSPNresults/37-result.txt

Large diffs are not rendered by default.

895 changes: 895 additions & 0 deletions 2020-EDCC/GreatSPNresults/38-result.txt

Large diffs are not rendered by default.

2,207 changes: 2,207 additions & 0 deletions 2020-EDCC/GreatSPNresults/39-result.txt

Large diffs are not rendered by default.

2,097 changes: 2,097 additions & 0 deletions 2020-EDCC/GreatSPNresults/40-result.txt

Large diffs are not rendered by default.

898 changes: 898 additions & 0 deletions 2020-EDCC/GreatSPNresults/41-result.txt

Large diffs are not rendered by default.

547 changes: 547 additions & 0 deletions 2020-EDCC/GreatSPNresults/42-result.txt

Large diffs are not rendered by default.

663 changes: 663 additions & 0 deletions 2020-EDCC/GreatSPNresults/43-result.txt

Large diffs are not rendered by default.

1,123 changes: 1,123 additions & 0 deletions 2020-EDCC/GreatSPNresults/44-result.txt

Large diffs are not rendered by default.

779 changes: 779 additions & 0 deletions 2020-EDCC/GreatSPNresults/45-result.txt

Large diffs are not rendered by default.

604 changes: 604 additions & 0 deletions 2020-EDCC/GreatSPNresults/46-result.txt

Large diffs are not rendered by default.

1,012 changes: 1,012 additions & 0 deletions 2020-EDCC/GreatSPNresults/47-result.txt

Large diffs are not rendered by default.

1,069 changes: 1,069 additions & 0 deletions 2020-EDCC/GreatSPNresults/48-result.txt

Large diffs are not rendered by default.

965 changes: 965 additions & 0 deletions 2020-EDCC/GreatSPNresults/49-result.txt

Large diffs are not rendered by default.

12,681 changes: 12,681 additions & 0 deletions 2020-EDCC/GreatSPNresults/50-result.txt

Large diffs are not rendered by default.

1,073 changes: 1,073 additions & 0 deletions 2020-EDCC/GreatSPNresults/51-result.txt

Large diffs are not rendered by default.

1,073 changes: 1,073 additions & 0 deletions 2020-EDCC/GreatSPNresults/52-result.txt

Large diffs are not rendered by default.

1,035 changes: 1,035 additions & 0 deletions 2020-EDCC/GreatSPNresults/53-result.txt

Large diffs are not rendered by default.

209 changes: 209 additions & 0 deletions 2020-EDCC/PythonScript/src/Bdmp2PNPRO.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,209 @@
#!/usrINPUT=Nonen
# def parse_result(file):
parse_state = 0
result = None
results = []
old = False
matching_lines = []


###############################################################
###############################################################
###############################################################
###############################################################
##########################################################reading the fi structure
def ReadFi(inputfile):
BDMP = {}
with open(inputfile, 'rt', encoding='latin-1') as file_object:
lines = file_object.readlines()
file_object.seek(0)
for i, line in enumerate(file_object):
if line.startswith("OBJECT"):
element = {}
match = re.search(r"OBJECT (.*) IS_A (.*);", line)
if (match.group(1) == 'OPTIONS') | (match.group(1) == '__ARBRE__EIRM') | (
match.group(2) == 'logic_link') | (match.group(2) == 'trigger_link') | (
match.group(2) == 'before_link'):
continue
else:
element = {'Name': match.group(1), 'Type': match.group(2)}
element_Name = match.group(1)
ref = i + 1
while not lines[ref].startswith("OBJECT"):
ref += 1
match = re.search(r"fathers\n", lines[ref])
if match:
element['Fathers'] = (lines[ref + 1].replace(';', '').split()[1:])
match = re.search(r"sons\n", lines[ref])
if match:
element['Sons'] = (lines[ref + 1].replace(';', '').split()[1:])
match = re.search(r"previous\n", lines[ref])
if match:
element['Previous'] = (lines[ref + 1].replace(';', '').split()[1:])
match = re.search(r"calculate_required\n", lines[ref])
if match:
element['Calculate'] = lines[ref + 2].split()[1].strip('\' ;')
match = re.search(r"mu\n", lines[ref])
if match:
element['Mu'] = lines[ref + 2].split()[1].strip(';')
match = re.search(r"lambda\n", lines[ref])
if match:
element['lambda'] = lines[ref + 2].split()[1].strip(';')
match = re.search(r"triggered_by\n", lines[ref])
if match:
element['Triggered_by'] = lines[ref + 1].split()[1].strip(';')
BDMP[element_Name] = element
############################# Prepreocessing components
for component in BDMP:
if not 'Sons' in BDMP[component]:
BDMP[component]['Sons'] = 'Null'
if not 'Fathers' in BDMP[component]:
BDMP[component]['Fathers'] = 'Null'
if not 'Triggered_by' in BDMP[component]:
BDMP[component]['Triggered_by'] = 'Null'
if not 'Previous' in BDMP[component]:
BDMP[component]['Previous'] = 'Null'
return BDMP
############################################################### Modularizing the BDMP###################
###############################################################
###############################################################
###############################################################
###############################################################

def Modularize(BDMP):
q = Queue()
s = deque()

##########get top elements BDMP is multitop tree
for component in BDMP:
if BDMP[component]['Fathers'] == 'Null':
s.append(BDMP[component]['Name'])
module = set()
children = {}
module_cnt = 0
while True:
while s:
vertex = s.pop()
children = (BDMP[vertex]['Sons'])
if children != 'Null':
for child in children:
if BDMP[child]['Triggered_by'] != 'Null' or BDMP[child]['Previous'] != 'Null':
q.put(child)
if (BDMP[child]['Sons'] != 'Null') and (BDMP[child]['Triggered_by'] == 'Null') and (BDMP[child]['Previous'] == 'Null'):
s.append(child)
if BDMP[child]['Sons'] == 'Null' and (BDMP[child]['Triggered_by'] == 'Null') and (BDMP[child]['Previous'] == 'Null'):
module.add(child)
if vertex not in module:
module.add(vertex)
else:
module.add(vertex)
for component in module:
if 'module' in BDMP[component]:
BDMP[component]['module'] = [BDMP[component]['module'], str(module_cnt)]
else:
BDMP[component]['module'] = str(module_cnt)
print(module_cnt, module)
module.clear()
module_cnt += 1
if q.empty():
break
if not q.empty():
s.append(q.get())
#print(BDMP['AND_1']['Fathers'])
return BDMP

######################################################################33Writing Modest Definitions
################################################################################################
################################################################################################
################################################################################################
################################################################################################
################################################################################################
def WriteModest(BDMP, inputfile, outputfile):
header = []
footer = []
header.append("//##########Automatically generated Modest file from: \"" + inputfile + "\"\n")
footer.append("//##########Composition of all processes\n")
footer.append("par\n{\n")
with open(outputfile, 'w+') as write_object:
module = set()
for element in BDMP:
if BDMP[element]['module'] not in module:
module.update(BDMP[element]['module'])
actions = []
actions.append("action")
for element in module:
actions.append("act_" + str(element) + ", dact_" + element + "\n") ################33
header.append(str(actions))
for element in BDMP:
#########################Exponential event
if BDMP[element]['Type'] == 'f_leaf':
header.append("action act_" + BDMP[element]['Name'] + ",dact_" + BDMP[element]['Name'] + ", fail_" +
BDMP[element]['Name'] + ", repaired_" + BDMP[element]['Name'] + ';\n')
header.append("bool " + BDMP[element]['Name'] + " = false;\n")
footer.append("::" + BDMP[element]['Name'] + BDMP[element]['Name'] + "() :: " + BDMP[element][
'Name'] + '_Act()\n')
write_object.write(
"//##########Failure Behavior of \"" + BDMP[element]['Type'] + "\" named \"" + BDMP[element][
'Name'] + '\"\n')
write_object.write("process " + BDMP[element]['Name'] + "(){" + '\n')
write_object.write(
"process P1() {alt{::dact_" + BDMP[element]['module'] + ";" + BDMP[element]['Name'] + "()::rate(" +
BDMP[element]['lambda'] +
") tau{=" + BDMP[element]['Name'] + "=true=}; fail_" + BDMP[element]['Name'] + "; P2()}}" + '\n')
write_object.write(
"process P2() " + "{alt{::dact_" + BDMP[element]['Name'] + "; " + "alt{::act_" + BDMP[element][
'Name'] + "; P2()::rate(" + BDMP[element]['Mu'] + ") tau{=" + BDMP[element]['Name'] +
"=false=}; repaired_" + BDMP[element]['Name'] + "; " + BDMP[element]['Name'] + "()}::rate(" +
BDMP[element]['Mu'] + ") tau{=" +
BDMP[element]['Name'] + "=false=}; repaired_" + BDMP[element]['Name'] + "; P1()}}" + '\n')
write_object.write("act_" + BDMP[element]['module'] + "; P1()}" + '\n')
write_object.write("//##########activation Behavior" + '\n')
write_object.write("process " + BDMP[element]['Name'] + "_Act(){" + '\n')
write_object.write(
"act_" + BDMP[element]['module'] + "; dact_" + BDMP[element]['module'] + "; " + BDMP[element][
'Name'] + "_Act()}\n")
#########################Top Level Event
if BDMP[element]['Type'] == 'undes_event':
header.append("action act_" + BDMP[element]['Name'] + ",dact_" + BDMP[element]['Name'] + ", fail_" +
BDMP[element][
'Name'] + ", repaired_" + BDMP[element]['Name'] + ';\n')
header.append("bool " + BDMP[element]['Name'] + " = false;\n")
footer.append(":: " + BDMP[element]['Name'] + "() :: " + BDMP[element]['Name'] + '_Act()\n')
write_object.write(
"//##########Failure Behavior of \"" + BDMP[element]['Type'] + "\" named \"" + BDMP[element][
'Name'] + '\"\n')
write_object.write("process " + BDMP[element]['Name'] + "() {" + '\n')
write_object.write(
"fail_" + BDMP[element]['Sons'][0] + " {= " + BDMP[element]['Name'] + "=true=} ; repaired_" +
BDMP[element]['Sons'][0] + " {= " + BDMP[element]['Name'] + "=false=}; " + BDMP[element][
'Name'] + "()\n }\n")
write_object.write("//##########activation Behavior" + '\n')
write_object.write("process " + BDMP[element]['Name'] + "_Act(){" + '\n')
write_object.write(
"act_" + BDMP[element]['Name'] + "; when(false) dact_" + BDMP[element]['Name'] + "; " +
BDMP[element][
'Name'] + "_Act()}\n")
#########################AND Gate
if BDMP[element]['Type'] == 'and_gate':
print("we have an and gate")
#########################Or Gate
if BDMP[element]['Type'] == 'or_gate':
print("we have an or gate")
write_object.seek(0, 0)
content = write_object.read()
write_object.seek(0, 0)
for row in header:
write_object.write(row)
write_object.write(content)
write_object.seek(0, 2)
for row in footer:
write_object.write(row)
write_object.write("}")








Loading

0 comments on commit 47559fc

Please sign in to comment.