Commit 9443e939 authored by Andrew's avatar Andrew
Browse files

Updated Edisyn. Made into an optional dependency with optional tests and added...

Updated Edisyn. Made into an optional dependency with optional tests and added install instructions.
parent 57c9f7f8
......@@ -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. 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" },
]
......@@ -17,6 +17,11 @@ dd = "^0.5.6"
tqdm = "^4.46.1"
colorama = {version = "^0.4.3", platform = "windows"}
# Optional dependencies for opacity verification and enforcement
# Edisyn
#edisyn = { version="^1.0.0", optional = true}
edisyn = {path = "../edisyn", optional = true, develop = true}
[tool.poetry.dev-dependencies]
pytest = "^5.2"
black = "^19.10b0"
......@@ -35,4 +40,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)
......
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