diff --git a/.readthedocs.yaml b/.readthedocs.yaml new file mode 100644 index 0000000..015eb5d --- /dev/null +++ b/.readthedocs.yaml @@ -0,0 +1,19 @@ +# Read the Docs configuration file for MkDocs projects +# See https://docs.readthedocs.io/en/stable/config-file/v2.html for details + +# Required +version: 2 + +# Set the version of Python and other tools you might need +build: + os: ubuntu-22.04 + tools: + python: "3.12" + +mkdocs: + configuration: mkdocs.yml + +# Optionally declare the Python requirements required to build your docs +python: + install: + - requirements: docs/requirements.txt diff --git a/LICENSE.txt b/LICENSE.txt new file mode 100644 index 0000000..3d6a5e4 --- /dev/null +++ b/LICENSE.txt @@ -0,0 +1,28 @@ +BSD 3-Clause License + +Copyright (c) 2024, California Institute of Technology + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md index 3040ad8..3b58304 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,11 @@ -# flowsynth +# Floras: Flow-Based Reactive Test Synthesis for Autonomous Systems -The flowsynth repository contains implementations of the algorithms developed in the following paper: +

+ +

-[Josefine B. Graebener*, Apurva S. Badithela*, Denizalp Goktas, Wyatt Ubellacker, Eric V. Mazumdar, Aaron D. Ames, and Richard M. Murray. "Flow-Based Synthesis of Reactive Tests for Discrete Decision-Making Systems with Temporal Logic Specifications." ArXiv abs/2404.09888 (2024).](https://arxiv.org/abs/2404.09888) \ No newline at end of file +Floras documentation can be found [here](https://floras.readthedocs.io). For installation instructions, please visit [this page](https://floras.readthedocs.io/en/latest/contributing/). + +The floras repository contains implementations of the algorithms developed in the following paper: + +[Josefine B. Graebener*, Apurva S. Badithela*, Denizalp Goktas, Wyatt Ubellacker, Eric V. Mazumdar, Aaron D. Ames, and Richard M. Murray. "Flow-Based Synthesis of Reactive Tests for Discrete Decision-Making Systems with Temporal Logic Specifications." ArXiv abs/2404.09888 (2024).](https://arxiv.org/abs/2404.09888) diff --git a/docs/automata.md b/docs/automata.md index 399c26b..7dd5c79 100644 --- a/docs/automata.md +++ b/docs/automata.md @@ -1 +1 @@ -::: flowsynth.components.automata +::: floras.components.automata diff --git a/docs/contributing.md b/docs/contributing.md index 5668ea0..32049a1 100644 --- a/docs/contributing.md +++ b/docs/contributing.md @@ -3,17 +3,22 @@ If you want to modify FLORAS or contribute, you can also install it directly from source. We are using pdm to manage the dependencies. ``` pip install pdm -git clone url +git clone https://github.com/tulip-control/flowsynth ``` Navigate to the repo and run to install the FLORAS and all required dependencies: ``` pdm install ``` -Next, enter the virtual environment created by pdm: +Next, install spot by running +``` +pdm run python get_spot.py +``` +To enter the virtual environment created by pdm: ``` $(pdm venv activate) ``` -New dependencies can be added by running: + +If you need to add dependencies you can do that by running: ``` pdm add your_dependency_here ``` diff --git a/docs/index.md b/docs/index.md index 9ed5698..11feccd 100644 --- a/docs/index.md +++ b/docs/index.md @@ -1,6 +1,13 @@ # FLORAS - Flow-based Reactive Test Synthesis for Autonomous Systems +
+ ![floras logo](logo.png "floras logo"){ width="300" } +
Welcome to FLORAS!
+
+ FLORAS is an open-source Python package for reactive test synthesis for autonomous systems using network flows. +Installation instructions can be found [here](contributing.md). + If you use FLORAS for research purposes, please acknowledge it by citing [Josefine B. Graebener\*, Apurva S. Badithela\*, Denizalp Goktas, Wyatt Ubellacker, Eric V. Mazumdar, Aaron D. Ames, and Richard M. Murray. "Flow-Based Synthesis of Reactive Tests for Discrete Decision-Making Systems with Temporal Logic Specifications." ArXiv abs/2404.09888 (2024).](https://arxiv.org/abs/2404.09888) diff --git a/docs/installing.md b/docs/installing.md index 03fe616..f6be9b6 100644 --- a/docs/installing.md +++ b/docs/installing.md @@ -1,15 +1,10 @@ # Installing FLORAS ### Requirements -FLORAS requires `Python>=3.10` and a C++17-compliant compiler (for example `g++>=7.0` or `clang++>=5.0`). +FLORAS requires `Python==3.10` and a C++17-compliant compiler (for example `g++>=7.0` or `clang++>=5.0`). You can check the versions by running `python --version` and `gcc --version`. -### From Pypi -FLORAS can be installed from Pypi as a standard Python package: -``` -pip install floras -``` ### From Source -If you want to modify FLORAS or contribute, you can also install it directly from source (see [here](contributing.md)). +If you want to modify FLORAS or contribute, you can install it directly from source (see [here](contributing.md)). ### Troubleshooting Here are common errors we encountered and what we learned to fix the problem. diff --git a/docs/logo.png b/docs/logo.png new file mode 100644 index 0000000..1e9a6ac Binary files /dev/null and b/docs/logo.png differ diff --git a/docs/optimization.md b/docs/optimization.md index a9b812e..46b741b 100644 --- a/docs/optimization.md +++ b/docs/optimization.md @@ -1 +1 @@ -::: flowsynth.optimization.optimization +::: floras.optimization.optimization diff --git a/docs/product.md b/docs/product.md index 58352e4..d08d333 100644 --- a/docs/product.md +++ b/docs/product.md @@ -1 +1 @@ -::: flowsynth.components.product +::: floras.components.product diff --git a/docs/requirements.txt b/docs/requirements.txt new file mode 100644 index 0000000..9283a65 --- /dev/null +++ b/docs/requirements.txt @@ -0,0 +1,2 @@ +mkdocs-material +mkdocstrings-python diff --git a/docs/transition_system.md b/docs/transition_system.md index 11f9450..0a6b266 100644 --- a/docs/transition_system.md +++ b/docs/transition_system.md @@ -1 +1 @@ -::: flowsynth.components.transition_system +::: floras.components.transition_system diff --git a/mkdocs.yml b/mkdocs.yml index 9d30351..cb35491 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -23,6 +23,9 @@ plugins: python: paths: [src] # search packages in the src folder +markdown_extensions: + - attr_list + - md_in_html copyright: > Copyright © 2024 - Caltech diff --git a/pdm.lock b/pdm.lock index 2d793f8..cf8d512 100644 --- a/pdm.lock +++ b/pdm.lock @@ -5,17 +5,17 @@ groups = ["default"] strategy = ["inherit_metadata"] lock_version = "4.5.0" -content_hash = "sha256:fe4ac9b8495cac5eaff1b6fd13c077ca0dd971ee3d13273299be9709b82befc5" +content_hash = "sha256:49837d73e6af3b303b328025645b7b986bf3c372683613e8274c69984b4695b2" [[metadata.targets]] -requires_python = ">=3.10" +requires_python = "==3.10" [[package]] name = "asttokens" version = "2.4.1" summary = "Annotate AST trees with source code positions" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" dependencies = [ "six>=1.12.0", "typing; python_version < \"3.5\"", @@ -306,7 +306,7 @@ version = "5.1.1" requires_python = ">=3.5" summary = "Decorators for Humans" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" files = [ {file = "decorator-5.1.1-py3-none-any.whl", hash = "sha256:b8c3f85900b9dc423225913c5aace94729fe1fa9763b38939a95226f02d37186"}, {file = "decorator-5.1.1.tar.gz", hash = "sha256:637996211036b6385ef91435e4fae22989472f9d571faba8927ba8253acbc330"}, @@ -330,7 +330,7 @@ version = "2.1.0" requires_python = ">=3.8" summary = "Get the currently executing AST node of a frame, and other information" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" files = [ {file = "executing-2.1.0-py2.py3-none-any.whl", hash = "sha256:8d63781349375b5ebccc3142f4b30350c0cd9c79f921cde38be2be4637e98eaf"}, {file = "executing-2.1.0.tar.gz", hash = "sha256:8ea27ddd260da8150fa5a708269c4a10e76161e2496ec3e587da9e3c0fe4b9ab"}, @@ -517,7 +517,7 @@ version = "8.27.0" requires_python = ">=3.10" summary = "IPython: Productive Interactive Computing" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" dependencies = [ "colorama; sys_platform == \"win32\"", "decorator", @@ -542,7 +542,7 @@ version = "0.19.1" requires_python = ">=3.6" summary = "An autocompletion tool for Python that can be used for text editors." groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" dependencies = [ "parso<0.9.0,>=0.8.3", ] @@ -756,7 +756,7 @@ version = "0.1.7" requires_python = ">=3.8" summary = "Inline Matplotlib backend for Jupyter" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" dependencies = [ "traitlets", ] @@ -1039,7 +1039,7 @@ version = "0.8.4" requires_python = ">=3.6" summary = "A Python Parser" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" files = [ {file = "parso-0.8.4-py2.py3-none-any.whl", hash = "sha256:a418670a20291dacd2dddc80c377c5c3791378ee1e8d12bffc35420643d43f18"}, {file = "parso-0.8.4.tar.gz", hash = "sha256:eb3a7b58240fb99099a345571deecc0f9540ea5f4dd2fe14c2a99d6b281ab92d"}, @@ -1061,7 +1061,7 @@ name = "pexpect" version = "4.9.0" summary = "Pexpect allows easy control of interactive console applications." groups = ["default"] -marker = "(sys_platform != \"win32\" and sys_platform != \"emscripten\") and python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\" and (sys_platform != \"win32\" and sys_platform != \"emscripten\")" dependencies = [ "ptyprocess>=0.5", ] @@ -1183,7 +1183,7 @@ version = "3.0.48" requires_python = ">=3.7.0" summary = "Library for building powerful interactive command lines in Python" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" dependencies = [ "wcwidth", ] @@ -1214,7 +1214,7 @@ name = "ptyprocess" version = "0.7.0" summary = "Run a subprocess in a pseudo terminal" groups = ["default"] -marker = "(sys_platform != \"win32\" and sys_platform != \"emscripten\") and python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\" and (sys_platform != \"win32\" and sys_platform != \"emscripten\")" files = [ {file = "ptyprocess-0.7.0-py2.py3-none-any.whl", hash = "sha256:4b41f3967fce3af57cc7e94b888626c18bf37a083e3651ca8feeb66d492fef35"}, {file = "ptyprocess-0.7.0.tar.gz", hash = "sha256:5c5d0a3b48ceee0b48485e0c26037c0acd7d29765ca3fbb5cb3831d347423220"}, @@ -1225,7 +1225,7 @@ name = "pure-eval" version = "0.2.3" summary = "Safely evaluate AST nodes without side effects" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" files = [ {file = "pure_eval-0.2.3-py3-none-any.whl", hash = "sha256:1db8e35b67b3d218d818ae653e27f06c3aa420901fa7b081ca98cbedc874e0d0"}, {file = "pure_eval-0.2.3.tar.gz", hash = "sha256:5f4e983f40564c576c7c8635ae88db5956bb2229d7e9237d03b3c0b0190eaf42"}, @@ -1545,7 +1545,7 @@ name = "stack-data" version = "0.6.3" summary = "Extract data from python stack frames and tracebacks for informative displays" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" dependencies = [ "asttokens>=2.1.0", "executing>=1.2.0", @@ -1574,7 +1574,7 @@ version = "5.14.3" requires_python = ">=3.8" summary = "Traitlets Python configuration system" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" files = [ {file = "traitlets-5.14.3-py3-none-any.whl", hash = "sha256:b74e89e397b1ed28cc831db7aea759ba6640cb3de13090ca145426688ff1ac4f"}, {file = "traitlets-5.14.3.tar.gz", hash = "sha256:9ed0579d3502c94b4b3732ac120375cda96f923114522847de4b3bb98b96b6b7"}, @@ -1605,7 +1605,7 @@ version = "4.12.2" requires_python = ">=3.8" summary = "Backported and Experimental Type Hints for Python 3.8+" groups = ["default"] -marker = "python_version < \"3.12\" and python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" files = [ {file = "typing_extensions-4.12.2-py3-none-any.whl", hash = "sha256:04e5ca0351e0f3f85c6853954072df659d0d13fac324d0072316b67d7794700d"}, {file = "typing_extensions-4.12.2.tar.gz", hash = "sha256:1a7ead55c7e559dd4dee8856e3a88b41225abfe1ce8df57b7c13915fe121ffb8"}, @@ -1661,7 +1661,7 @@ name = "wcwidth" version = "0.2.13" summary = "Measures the displayed width of unicode strings in a terminal" groups = ["default"] -marker = "python_version > \"3.6\"" +marker = "python_version > \"3.6\" and python_version < \"3.11\"" dependencies = [ "backports-functools-lru-cache>=1.2.1; python_version < \"3.2\"", ] diff --git a/pyproject.toml b/pyproject.toml index 3b3073c..f1c43c0 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -3,10 +3,10 @@ requires = ["pdm-backend"] build-backend = "pdm.backend" [project] -name = "flowsynth" +name = "floras" description = "A package for network flow-based test synthesis." authors = [ - {name = "flowsynth developers", email = "tbd"}, + {name = "floras developers", email = "tbd"}, ] license = {text = "BSD-3-Clause"} classifiers = [ @@ -30,10 +30,13 @@ dependencies = [ "pytest>=8.3.3", "coverage>=7.6.1", "pygraphviz>=1.13", + "graphviz>=0.20.3", ] -requires-python = ">=3.10" +requires-python = "==3.10" version = "0.0.0" readme = "README.md" [project.scripts] -from_json = "flowsynth.main:main" +from_json = "floras.main:main" + +[tool.pdm] diff --git a/src/flowsynth/components/automata.py b/src/floras/components/automata.py similarity index 99% rename from src/flowsynth/components/automata.py rename to src/floras/components/automata.py index e9203ea..672ecf2 100644 --- a/src/flowsynth/components/automata.py +++ b/src/floras/components/automata.py @@ -8,7 +8,7 @@ from collections import OrderedDict as od import re import os -from flowsynth.components.utils import powerset, neg, conjunction, disjunction +from floras.components.utils import powerset, neg, conjunction, disjunction class Automaton: diff --git a/src/flowsynth/components/product.py b/src/floras/components/product.py similarity index 98% rename from src/flowsynth/components/product.py rename to src/floras/components/product.py index 7f7ca34..5e31b8a 100644 --- a/src/flowsynth/components/product.py +++ b/src/floras/components/product.py @@ -8,8 +8,8 @@ import os import networkx as nx from itertools import product -from flowsynth.components.transition_system import TranSys -from flowsynth.components.automata import Automaton +from floras.components.transition_system import TranSys +from floras.components.automata import Automaton spot.setup(show_default='.tvb') diff --git a/src/flowsynth/components/transition_system.py b/src/floras/components/transition_system.py similarity index 100% rename from src/flowsynth/components/transition_system.py rename to src/floras/components/transition_system.py diff --git a/src/flowsynth/components/utils.py b/src/floras/components/utils.py similarity index 100% rename from src/flowsynth/components/utils.py rename to src/floras/components/utils.py diff --git a/src/flowsynth/main.py b/src/floras/main.py similarity index 87% rename from src/flowsynth/main.py rename to src/floras/main.py index 5e61a62..04946f8 100644 --- a/src/flowsynth/main.py +++ b/src/floras/main.py @@ -2,11 +2,11 @@ import ast import argparse -from flowsynth.optimization.optimize import solve -from flowsynth.components.automata import get_system_automaton, get_tester_automaton, get_product_automaton -from flowsynth.components.transition_system import TranSys, TransitionSystemInput -from flowsynth.components.product import sync_prod -from flowsynth.components.utils import get_states_and_transitions_from_file +from floras.optimization.optimize import solve +from floras.components.automata import get_system_automaton, get_tester_automaton, get_product_automaton +from floras.components.transition_system import TranSys, TransitionSystemInput +from floras.components.product import sync_prod +from floras.components.utils import get_states_and_transitions_from_file from ipdb import set_trace as st diff --git a/src/flowsynth/optimization/optimization.py b/src/floras/optimization/optimization.py similarity index 99% rename from src/flowsynth/optimization/optimization.py rename to src/floras/optimization/optimization.py index a431151..889424f 100644 --- a/src/flowsynth/optimization/optimization.py +++ b/src/floras/optimization/optimization.py @@ -5,7 +5,7 @@ import time import numpy as np import networkx as nx -from flowsynth.optimization.utils import find_map_G_S +from floras.optimization.utils import find_map_G_S from gurobipy import * from copy import deepcopy import os diff --git a/src/flowsynth/optimization/optimize.py b/src/floras/optimization/optimize.py similarity index 72% rename from src/flowsynth/optimization/optimize.py rename to src/floras/optimization/optimize.py index 843ed27..7478b16 100644 --- a/src/flowsynth/optimization/optimize.py +++ b/src/floras/optimization/optimize.py @@ -1,5 +1,5 @@ -from flowsynth.optimization.setup_graphs import setup_nodes_and_edges -from flowsynth.optimization.optimization import MILP +from floras.optimization.setup_graphs import setup_nodes_and_edges +from floras.optimization.optimization import MILP from ipdb import set_trace as st diff --git a/src/flowsynth/optimization/setup_graphs.py b/src/floras/optimization/setup_graphs.py similarity index 100% rename from src/flowsynth/optimization/setup_graphs.py rename to src/floras/optimization/setup_graphs.py diff --git a/src/flowsynth/optimization/utils.py b/src/floras/optimization/utils.py similarity index 100% rename from src/flowsynth/optimization/utils.py rename to src/floras/optimization/utils.py diff --git a/src/flowsynth/optimization/milp_static.py b/src/flowsynth/optimization/milp_static.py deleted file mode 100644 index 2924395..0000000 --- a/src/flowsynth/optimization/milp_static.py +++ /dev/null @@ -1,229 +0,0 @@ -''' -Gurobipy implementation of the MILP for static obstacles. -''' -from gurobipy import GRB -import time -import numpy as np -from ipdb import set_trace as st -import networkx as nx -from src.flowsynth.optimization.utils import find_map_G_S -from gurobipy import * -from copy import deepcopy -import os -import json - -# Callback function -def cb(model, where): - if where == GRB.Callback.MIPNODE: - # Get model objective - obj = model.cbGet(GRB.Callback.MIPNODE_OBJBST) # Current best objective - sol_count = model.cbGet(GRB.Callback.MIPNODE_SOLCNT) # No. of feasible solns found. - - # Has objective changed? - if abs(obj - model._cur_obj) > 1e-8: - # If so, update incumbent - model._cur_obj = obj - - # Terminate if objective has not improved in 60s - # Current objective is less than infinity. - - if sol_count >= 1: - if time.time() - model._time > 60: - model._data["term_condition"] = "Obj not changing" - model.terminate() - else: - # Total termination time if the optimizer has not found anything in 5 min: - if time.time() - model._time > 600: - model._data["term_condition"] = "Timeout" - model.terminate() - -# Gurobi implementation -def solve_opt_static(GD, SD, callback="cb", logger=None, logger_runtime_dict=None): - cleaned_intermed = [x for x in GD.acc_test if x not in GD.acc_sys] - # create G and remove self-loops - G = GD.graph - to_remove = [] - for i, j in G.edges: - if i == j: - to_remove.append((i,j)) - G.remove_edges_from(to_remove) - - # remove intermediate nodes - G_minus_I = deepcopy(G) - G_minus_I.remove_nodes_from(cleaned_intermed) - - # create S and remove self-loops - S = SD.graph - to_remove = [] - for i, j in S.edges: - if i == j: - to_remove.append((i,j)) - S.remove_edges_from(to_remove) - - model_edges = list(G.edges) - model_nodes = list(G.nodes) - model_edges_without_I = list(G_minus_I.edges) - model_nodes_without_I = list(G_minus_I.nodes) - - src = GD.init - sink = GD.sink - inter = cleaned_intermed - - # for the flow on S - map_G_to_S = find_map_G_S(GD,SD) - - s_sink = SD.acc_sys - s_src = SD.init[0] - - - model_s_edges = list(S.edges) - model_s_nodes = list(S.nodes) - - model = Model() - # Define variables - f = model.addVars(model_edges, name="flow") - m = model.addVars(model_nodes_without_I, name="m") - d = model.addVars(model_edges, vtype=GRB.BINARY, name="d") - - # Define Objective - term = sum(f[i,j] for (i, j) in model_edges if i in src) - ncuts = sum(d[i,j] for (i, j) in model_edges) - reg = 1/len(model_edges) - model.setObjective(term - reg*ncuts, GRB.MAXIMIZE) - - # Define constraints - # Nonnegativity - lower bounds - model.addConstrs((d[i, j] >= 0 for (i,j) in model_edges), name='d_nonneg') - model.addConstrs((m[i] >= 0 for i in model_nodes_without_I), name='mu_nonneg') - model.addConstrs((f[i, j] >= 0 for (i,j) in model_edges), name='f_nonneg') - - # upper bounds - model.addConstrs((d[i, j] <= 1 for (i,j) in model_edges), name='d_upper_b') - model.addConstrs((m[i] <= 1 for i in model_nodes_without_I), name='mu_upper_b') - # capacity (upper bound for f) - model.addConstrs((f[i, j] <= 1 for (i,j) in model_edges), name='capacity') - - # preserve flow of at least 1 - model.addConstr((1 <= sum(f[i,j] for (i, j) in model_edges if i in src)), name='conserve_F') - - # conservation - model.addConstrs((sum(f[i,j] for (i,j) in model_edges if j == l) == sum(f[i,j] for (i,j) in model_edges if i == l) for l in model_nodes if l not in src and l not in sink), name='conservation') - - # no flow into source or out of sink - model.addConstrs((f[i,j] == 0 for (i,j) in model_edges if j in src or i in sink), name="no_out_sink_in_src") - - # cut constraint (cut edges have zero flow) - model.addConstrs((f[i,j] + d[i,j] <= 1 for (i,j) in model_edges), name='cut_cons') - - # source sink partitions - for i in model_nodes_without_I: - for j in model_nodes_without_I: - if i in src and j in sink: - model.addConstr(m[i] - m[j] >= 1) - - # max flow cut constraint (cut variable d partitions the groups) - model.addConstrs((d[i,j] - m[i] + m[j] >= 0 for (i,j) in model_edges_without_I)) - - # --------- map static obstacles to other edges in G - for count, (i,j) in enumerate(model_edges): - out_state = GD.node_dict[i][0] - in_state = GD.node_dict[j][0] - for (imap,jmap) in model_edges[count+1:]: - if out_state == GD.node_dict[imap][0] and in_state == GD.node_dict[jmap][0]: - model.addConstr(d[i, j] == d[imap, jmap]) - - - # --------- add bidirectional cuts on G - for count, (i,j) in enumerate(model_edges): - out_state = GD.node_dict[i][0] - in_state = GD.node_dict[j][0] - for (imap,jmap) in model_edges[count+1:]: - if in_state == GD.node_dict[imap][0] and out_state == GD.node_dict[jmap][0]: - model.addConstr(d[i, j] == d[imap, jmap]) - - # --------- set parameters - # Last updated objective and time (for callback function) - model._cur_obj = float('inf') - model._time = time.time() - model.Params.Seed = np.random.randint(0,100) - - # store model data for logging - model._data = dict() - model._data["term_condition"] = None - - # optimize - if callback=="cb": - t0 = time.time() - model.optimize(callback=cb) - tf = time.time() - delt = tf - t0 - else: - t0 = time.time() - model.optimize() - tf = time.time() - delt = tf - t0 - - model._data["runtime"] = model.Runtime - model._data["flow"] = None - model._data["ncuts"] = None - - # Storing problem variables: - model._data["n_bin_vars"] = model.NumBinVars - model._data["n_cont_vars"] = model.NumVars - model.NumBinVars - model._data["n_constrs"] = model.NumConstrs - - f_vals = [] - d_vals = [] - flow = None - exit_status = None - - if model.status == 4: - model.Params.DualReductions = 0 - exit_status = 'inf' - model._data["status"] = "inf/unbounded" - return 0,0,exit_status - elif model.status == 11 and model.SolCount < 1: - exit_status = 'not solved' - model._data["status"] = "not_solved" - model._data["exit_status"] = exit_status - elif model.status == 2 or (model.status == 11 and model.SolCount >= 1): - if model.status == 2: - model._data["status"] = "optimal" - model._data["term_condition"] = "optimal found" - else: - # feasible. maybe be optimal. - model._data["status"] = "feasible" - - # --------- parse output - d_vals = dict() - f_vals = dict() - - for (i,j) in model_edges: - f_vals.update({(i,j): f[i,j].X}) - for (i,j) in model_edges: - d_vals.update({(i,j): d[i,j].X}) - - flow = sum(f[i,j].X for (i,j) in model_edges if i in src) - model._data["flow"] = flow - ncuts = 0 - - for key in d_vals.keys(): - if d_vals[key] > 0.9: - ncuts+=1 - print('{0} to {1} at {2}'.format(GD.node_dict[key[0]], GD.node_dict[key[1]],d_vals[key])) - - model._data["ncuts"] = ncuts - exit_status = 'opt' - model._data["exit_status"] = exit_status - elif model.status == 3: - exit_status = 'inf' - model._data["status"] = "inf" - else: - st() - - if not os.path.exists("log"): - os.makedirs("log") - with open('log/opt_data.json', 'w') as fp: - json.dump(model._data, fp) - - return d_vals, flow, exit_status diff --git a/tests/test_1.py b/tests/test_1.py deleted file mode 100644 index a82a438..0000000 --- a/tests/test_1.py +++ /dev/null @@ -1,63 +0,0 @@ -"""Testing current code.""" -import pytest - -import sys -sys.path.append('../') -from flowsynth.components.automata import get_system_automaton, get_tester_automaton, get_product_automaton -from flowsynth.components.transition_system import TransitionSystemInput, TranSys -from flowsynth.components.product import sync_prod -from flowsynth.optimization.optimize import solve - -def test_sample(): - states_list = [0,1,2,3,4,5] - transitions_dict = {0: [1,2,3], 1: [2,3,4], 2: [3,4,5], 3: [4], 4: [5,0], 5: [5]} - labels_dict = {0 : ['a'], 5: ['goal'], 3: ['int']} - init_list = [0] - - transition_system_input = TransitionSystemInput(states_list, transitions_dict, labels_dict, init_list) - - sys_formula = 'F(goal)' - test_formula = 'F(int)' - - # get automata - sys_aut, spot_aut_sys = get_system_automaton(sys_formula) - test_aut, spot_aut_test = get_tester_automaton(test_formula) - prod_aut = get_product_automaton(spot_aut_sys, spot_aut_test) - - # get transition system - transys = TranSys(transition_system_input) - - # get virtual graphs - virtual_sys = sync_prod(transys, sys_aut) - virtual = sync_prod(transys, prod_aut) - - d, flow = solve(virtual, transys, prod_aut, virtual_sys, case = 'static') - - assert flow >= 1.0 - -if __name__=='__main__': - states_list = [0,1,2,3,4,5] - transitions_dict = {0: [1,2,3], 1: [2,3,4], 2: [3,4,5], 3: [4], 4: [5,0], 5: [5]} - labels_dict = {0 : ['a'], 5: ['goal'], 3: ['int']} - init_list = [0] - - transition_system_input = TransitionSystemInput(states_list, transitions_dict, labels_dict, init_list) - - sys_formula = 'F(goal)' - test_formula = 'F(int)' - - # get automata - sys_aut, spot_aut_sys = get_system_automaton(sys_formula) - test_aut, spot_aut_test = get_tester_automaton(test_formula) - prod_aut = get_product_automaton(spot_aut_sys, spot_aut_test) - - # get transition system - transys = TranSys(transition_system_input) - - # get virtual graphs - virtual_sys = sync_prod(transys, sys_aut) - virtual = sync_prod(transys, prod_aut) - - d, flow = solve(virtual, transys, prod_aut, virtual_sys, case = 'static') - - assert flow >= 1.0 diff --git a/tests/test_reactive_1.py b/tests/test_reactive_1.py index 1be1f68..3cc2640 100644 --- a/tests/test_reactive_1.py +++ b/tests/test_reactive_1.py @@ -3,10 +3,10 @@ import sys sys.path.append('../') -from flowsynth.components.automata import get_system_automaton, get_tester_automaton, get_product_automaton -from flowsynth.components.transition_system import TransitionSystemInput, TranSys -from flowsynth.components.product import sync_prod -from flowsynth.optimization.optimize import solve +from floras.components.automata import get_system_automaton, get_tester_automaton, get_product_automaton +from floras.components.transition_system import TransitionSystemInput, TranSys +from floras.components.product import sync_prod +from floras.optimization.optimize import solve def test_reactive(): states_list = ['init', 'd1', 'd2', 'int_goal', 'p1', 'p2', 'goal'] diff --git a/tests/test_static_1.py b/tests/test_static_1.py new file mode 100644 index 0000000..90af25c --- /dev/null +++ b/tests/test_static_1.py @@ -0,0 +1,36 @@ +"""Testing current code in static setup.""" +import pytest + +import sys +sys.path.append('../') +from floras.components.automata import get_system_automaton, get_tester_automaton, get_product_automaton +from floras.components.transition_system import TransitionSystemInput, TranSys +from floras.components.product import sync_prod +from floras.optimization.optimize import solve + +def test_static(): + states_list = [0,1,2,3,4,5] + transitions_dict = {0: [1,2,3], 1: [2,3,4], 2: [3,4,5], 3: [4], 4: [5,0], 5: [5]} + labels_dict = {0 : ['a'], 5: ['goal'], 3: ['int']} + init_list = [0] + + transition_system_input = TransitionSystemInput(states_list, transitions_dict, labels_dict, init_list) + + sys_formula = 'F(goal)' + test_formula = 'F(int)' + + # get automata + sys_aut, spot_aut_sys = get_system_automaton(sys_formula) + test_aut, spot_aut_test = get_tester_automaton(test_formula) + prod_aut = get_product_automaton(spot_aut_sys, spot_aut_test) + + # get transition system + transys = TranSys(transition_system_input) + + # get virtual graphs + virtual_sys = sync_prod(transys, sys_aut) + virtual = sync_prod(transys, prod_aut) + + d, flow = solve(virtual, transys, prod_aut, virtual_sys, case = 'static') + + assert flow >= 1.0