Commit 792d5dc1 authored by Andrew Richard Wintenberg's avatar Andrew Richard Wintenberg
Browse files

Added Matthew's contact tracing script and fixed bosy command

parent 16a32f55
......@@ -20,7 +20,7 @@ from DESops.opacity.bosy.spin import ltl2spin, read_spin, write_spin
# Change the path to Bosy here appropriately
bosy_path = "/".join([str(Path.home()), "libraries/bosy"])
# Also ensure that Aiger is installed at the following path
aiger_path = "/".join([str(Path.home()), "libraries/aiger-1.9.9"])
aiger_path = "/".join([str(Path.home()), "libraries/aiger"])
# Note there are currently some issues with non-absolute paths
......@@ -167,17 +167,20 @@ def run_bosy(
def synthesize_bosy(bosy_path, aag_path):
def synthesize_bosy(i_bosy_path, i_aag_path):
Synthesize a controller from hyperLTL specifications using bosy.
bosy_path: the path for the input bosy file
aag_path: the path for the Aiger (.aag) file
i_bosy_path: the path for the input bosy file
i_aag_path: the path for the Aiger (.aag) file
print(os.popen("echo $PATH").read())
#print(os.popen("echo $PATH").read())
# f"swift run -c release BoSyHyper --synthesize {i_bosy_path} | sed -ne '/^aag.*/,$ p' > {i_aag_path}"
f"swift run -c release BoSyHyper --synthesize {bosy_path} | sed -ne '/^aag.*/,$ p' > {aag_path}"
f".build/release/BoSyHyper --synthesize {i_bosy_path} | sed -ne '/^aag.*/,$ p' > {i_aag_path}"
import datetime
import os
import DESops as d
from DESops.opacity.bosy.bosy_interface import run_bosy
from DESops.opacity.bosy.parse_smv import read_smv
from DESops.opacity.bosy.verify import verify_edit_function
from DESops.opacity.contact_tracing.generate_contact_model import contact_example
# choose between running full synthesis, or just parsing existing SMV file
run_synthesis = True
# choose between custom LTL or standard always inference
use_ltl = False
# choose whether we should attempt to simplify transitions using SymPy
simplify = False
if not os.path.exists('contact'):
# model parameters
map_file = "map1.fsm"
num_agents = 2
ids = list(range(num_agents))
pairs = [str(i) + str(j) for i in ids for j in ids if i < j]
base_path = "contact/cntl"
# generate and save model
g, event_var_maps = contact_example(map_file, num_agents)
d.write_fsm("contact/sys.fsm", g)
events = sorted(list(
inf_vars = [f"c_{p}" for p in pairs]
if use_ltl:
# generate LTL expression that requires that contact is eventually inferred
inf_fun = None
ltl_spec = list()
for p in pairs:
inf_var = f"c_{p}"
contact_events = [e for e in events if p in e]
ltl_spec.append(f"(!{inf_var} W ({' || '.join(contact_events)}))")
ltl_spec.append(f"(F({' || '.join(contact_events)}) -> F({inf_var}))")
# generate functions that return inferences about whether the current event includes a specific contact pair
ltl_spec = None
inf_fun = list()
for p in pairs:
inf_var = f"c_{p}"
inf_fun.append(lambda x, e: f"{inf_var}" if p in e else f"!{inf_var}")
# generate valid replacements sets for each event
valid_replaces = dict()
for e_i in events:
# observer location should match
valid_replaces[e_i] = {e_o for e_o in events if e_o[1] == e_i[1]}
if run_synthesis:
os.environ["PATH"] += os.pathsep + "/usr/local/swift/bin/"
print(f"Synthesis start: {}\n")
cntl, preds = run_bosy(
print(f"Synthesis end: {}\n")
cntl, preds = read_smv(
success = verify_edit_function(g, cntl)
if success:
print("Successful obfuscation")
print("Obfsucation failed")
# save output automata
d.write_fsm(base_path + ".fsm", cntl)
for inf, pred in preds.items():
pred.vs["marked"] = pred.vs["secret"]
d.write_fsm(f"contact/pred_{inf}.fsm", pred)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment