Commit 9d655724 authored by Andrew's avatar Andrew
Browse files

Merge branch 'test_merge'

parents b2dd0055 59f26f9a
......@@ -112,7 +112,7 @@ def supremal_sublanguage(
return H
def check_normality(H: DFA, G_obs_names: DFA, max_processes: int) -> StateSet:
def check_normality(H: DFA, G_obs_names: List[str], max_processes: int) -> StateSet:
"""
Check the normality condition of states H and returns states violating the condition.
"""
......@@ -121,22 +121,29 @@ def check_normality(H: DFA, G_obs_names: DFA, max_processes: int) -> StateSet:
bad_states = set()
all_H_names = H.vs["name"]
with ProcessPoolExecutor(mp_context=mp.get_context('fork'),max_workers=max_processes) as executor:
futures = []
try:
with ProcessPoolExecutor(mp_context=mp.get_context('fork'),max_workers=max_processes) as executor:
futures = []
chk = ceil(H.vcount() / max_processes)
for i, H_indecies in enumerate(pydash.chunk(range(H.vcount()), chk)):
futures.append(
executor.submit(
__find_bad_states_normal,
H_indecies,
G_obs_names,
all_H_names,
i + 1,
)
)
for f in as_completed(futures):
bad_states |= f.result()
except ValueError:
chk = ceil(H.vcount() / max_processes)
for i, H_indecies in enumerate(pydash.chunk(range(H.vcount()), chk)):
futures.append(
executor.submit(
__find_bad_states_normal,
H_indecies,
G_obs_names,
all_H_names,
i + 1,
)
)
bad_states |= __find_bad_states_normal(H_indecies, G_obs_names, all_H_names, i + 1)
for f in as_completed(futures):
bad_states |= f.result()
return bad_states
......@@ -162,7 +169,7 @@ def __find_bad_states_normal(
return bad_states
def check_controllability(H: DFA, G: DFA, max_processes: int) -> StateSet:
def check_controllability(H: DFA, G: List[str], max_processes: int) -> StateSet:
"""
Check the controllability condition of states in H and returns states violating the condition.
"""
......@@ -176,23 +183,30 @@ def check_controllability(H: DFA, G: DFA, max_processes: int) -> StateSet:
bad_states = set()
Euc = G.Euc
with ProcessPoolExecutor(mp_context=mp.get_context('fork'),max_workers=max_processes) as executor:
futures = []
try:
with ProcessPoolExecutor(mp_context=mp.get_context('fork'),max_workers=max_processes) as executor:
futures = []
chk = ceil(len(H_all_states) / max_processes)
for i, H_names in enumerate(pydash.chunk(list(H_all_states.keys()), chk)):
futures.append(
executor.submit(
__find_bad_states_controllable,
H_names,
H_all_states,
G_all_states,
Euc,
i + 1,
)
)
for f in as_completed(futures):
bad_states |= f.result()
except ValueError:
chk = ceil(len(H_all_states) / max_processes)
for i, H_names in enumerate(pydash.chunk(list(H_all_states.keys()), chk)):
futures.append(
executor.submit(
__find_bad_states_controllable,
H_names,
H_all_states,
G_all_states,
Euc,
i + 1,
)
)
bad_states |= __find_bad_states_controllable(H_names, H_all_states, G_all_states, Euc, i + 1)
for f in as_completed(futures):
bad_states |= f.result()
return bad_states
......
......@@ -4,19 +4,19 @@ implemented, including parallel/product compositions and observer computation. T
## Installation
Below is a diagram that showcases the installation process. Before installing DESops, the first three steps must be completed first.
Below is a diagram that showcases the installation process. Before installing DESops, the first three steps must be completed first.
![README_diagram graph image](img/diagram.png)
### Step 1: Clone Repository
On the right hand corner of this page, click on the blue box that says `Clone`. Copy and paste the HTTPS url.
On the right hand corner of this page, click on the blue box that says `Clone`. Copy and paste the HTTPS url.
In your working directory, write the following command:
$ git clone https://gitlab.eecs.umich.edu/M-DES-tools/desops.git
After running this command, a copy of this repository will be available in your working directory.
After running this command, a copy of this repository will be available in your working directory.
### Step 2: Install pkg-config and cairo
......@@ -78,6 +78,21 @@ The following is only relevant for using the `random_DFA` submodule.
There are detailed instructions for compiling the source code in the file `random_DFA/regal-1.08.0929/regal_readme.txt`
There are several required libraries, and a c++ compiler is needed to build the REGAL executables. The script `build.py` (only for Linux systems with a g++ compiler) automates the build process after the preqrequisite libraries are installed.
#### Opacity enforcement
Two methods for synthesizing enforcement mechanisms for opacity are currently supported. The first requires the optional
python library [EdiSyn](https://gitlab.eecs.umich.edu/M-DES-tools/EdiSyn). To install EdiSyn in an appropriate directory
, run:
$ git clone https://gitlab.eecs.umich.edu/M-DES-tools/EdiSyn.git
Then edit `pyproject.toml` to point to this directory. You will need to uncomment this line. For development EdiSyn can be used in the editable mode.
Finally, to use this optional dependency, use the command:
$ poetry install --extras "opacity_enf"
The second method for opacity enforcement uses the library BoSy. See (/DESops/opacity/bosy) for more details.
## Contributing to DESops
You will need [Poetry](https://python-poetry.org/) to start contribution on the DESops codes.
......
This diff is collapsed.
......@@ -2,7 +2,7 @@
name = "DESops"
version = "20.9.2"
description = ""
authors = ["Jack Weitze <jweitze@umich.edu>", "Romulo Meira Goes <r.meiragoes@gmail.com>", "Shoma Matsui <smatsui@umich.edu>"]
authors = ["Jack Weitze <jweitze@umich.edu>", "Romulo Meira Goes <r.meiragoes@gmail.com>", "Shoma Matsui <smatsui@umich.edu>", "Andrew Wintenberg <awintenb@umich.edu>"]
packages = [
{ include = "DESops" },
]
......@@ -16,6 +16,12 @@ requests = "^2.24.0"
dd = "^0.5.6"
tqdm = "^4.46.1"
colorama = {version = "^0.4.3", platform = "windows"}
"boolean.py" = "^4.0"
# Optional dependencies for opacity verification and enforcement
# Edisyn
# uncomment the next line if you have installed edisyn locally
# edisyn = {path = "../edisyn", optional = true, develop = true}
[tool.poetry.dev-dependencies]
pytest = "^5.2"
......@@ -35,4 +41,5 @@ requires = ["poetry>=0.12"]
build-backend = "poetry.masonry.api"
[tool.poetry.extras]
caching=["pycairo"]
caching = ["pycairo"]
opacity_enf = ["edisyn"]
import DESops as d
from DESops.opacity.edisyn_interface import enforce_state_based_opacity_edisyn
try:
from DESops.opacity.edisyn_interface import enforce_state_based_opacity_edisyn
edisyn_available = True
except ImportError:
edisyn_available = False
import pytest
@pytest.mark.skipif(not edisyn_available, reason="EdiSyn not available")
def test_simple_example():
g = d.automata.DFA()
g.add_vertices(2)
......@@ -30,7 +37,7 @@ def test_simple_example():
assert obf is None
@pytest.mark.skipif(not edisyn_available, reason="EdiSyn not available")
def test_k_step_example():
g = d.automata.NFA()
g.add_vertices(5)
......@@ -73,6 +80,7 @@ def l1_dist(p1, p2):
return max(abs(p1[0] - p2[0]), abs(p1[1] - p2[1]))
@pytest.mark.skipif(not edisyn_available, reason="EdiSyn not available")
def test_square_examples():
g, utility = gen_square_example(3, 3, 2)
obf = enforce_state_based_opacity_edisyn(g, utility, 'KSTEP', k=2, insertion_bound=1, joint=False)
......
import DESops as d
import DESops.SDA.event_extensions as ee
from DESops.opacity.edisyn_interface import enforce_state_based_opacity_edisyn
try:
from DESops.opacity.edisyn_interface import enforce_state_based_opacity_edisyn
edisyn_available = True
except ImportError:
edisyn_available = False
from DESops.opacity.secret_observer import construct_secret_observer_label_transform, tmp_verify_edit_opacity
from DESops.opacity.observation_map import StaticMask, NonDetDynamicMask
from DESops.opacity.language_functions import language_inclusion
import pytest
def test_edit_auto():
g = d.NFA()
g.add_vertices(2)
......@@ -48,6 +57,7 @@ def test_edit_auto():
assert language_inclusion(edited_g, target_auto, target_auto.events - target_auto.Euo)
@pytest.mark.skipif(not edisyn_available, reason="EdiSyn not available")
def test_edisyn_edit():
g = d.NFA()
g.add_vertices(4)
......
......@@ -13,4 +13,7 @@ def test_graph_algs():
ata_inf.set_weak_buchi(ata_inf.states)
ata_inf.simplify()
print(graph_algs.SCCHelper(ata_inf).computeSCC())
scc = graph_algs.SCCHelper(ata_inf.construct_transition_NFA()).computeSCC()
assert len(scc) == 2
assert {"p"} in scc
assert {"q"} in scc
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