Commit b6fad2b5 authored by romulo's avatar romulo
Browse files

Merge branch 'disable_DFA_check' into 'master'

Disable dfa check

See merge request !5
parents ae164e7c c5e2dda7
......@@ -145,5 +145,9 @@ static
# Examples romulo
Examples/
# VS code files and DS_STORE
.vscode/
.DS_Store
#pycharm stuff
.idea/
......@@ -20,4 +20,4 @@ from DESops.visualization.plot import plot
from DESops.visualization.write_svg import write_svg
from DESops.diagnoser import diagnoser
__version__ = "20.6.1a4"
__version__ = "20.9.2"
......@@ -93,7 +93,10 @@ def product(*automata: DFA) -> DFA:
[v["marked"] for v in G_out_vertices],
)
G_out.add_edges(
[e["pair"] for e in G_out_edges], [e["label"] for e in G_out_edges]
[e["pair"] for e in G_out_edges],
[e["label"] for e in G_out_edges],
check_DFA=False,
fill_out=True,
)
G_out.events = G1.events | G2.events
G_out.Euc.update(G1.Euc | G2.Euc)
......@@ -314,7 +317,10 @@ def parallel(*automata: DFA) -> DFA:
[v["marked"] for v in G_out_vertices],
)
G_out.add_edges(
[e["pair"] for e in G_out_edges], [e["label"] for e in G_out_edges]
[e["pair"] for e in G_out_edges],
[e["label"] for e in G_out_edges],
check_DFA=False,
fill_out=True,
)
G_out.events = G1.events | G2.events
G_out.Euc.update(G1.Euc | G2.Euc)
......@@ -564,8 +570,13 @@ def observer(G: Automata_t) -> Automata_t:
observer.Euc.update(G.Euc - G.Euo)
observer.Euo.clear()
observer.vs["marked"] = marked_list
observer.add_edges(transition_list, transition_label, fill_out=False)
observer.add_edges(
transition_list, transition_label, check_DFA=False, fill_out=False
)
observer.vs["out"] = outgoing_list
observer.vs["name"] = [tuple(v) for v in observer.vs["name"]]
return observer
......@@ -595,6 +606,7 @@ def strict_subautomata(H: DFA, G: DFA, skip_H_tilde=False) -> Tuple[Optional[DFA
A.add_edges(
[edge["pair"] for edge in edges_to_dead],
[edge["label"] for edge in edges_to_dead],
check_DFA=False,
fill_out=True,
)
......@@ -604,6 +616,7 @@ def strict_subautomata(H: DFA, G: DFA, skip_H_tilde=False) -> Tuple[Optional[DFA
A.add_edges(
[edge["pair"] for edge in dead_selfloops],
[edge["label"] for edge in dead_selfloops],
check_DFA=False,
fill_out=True,
)
......
from concurrent.futures import ProcessPoolExecutor, as_completed
import multiprocessing as mp
from enum import Enum, auto
from os import cpu_count
from math import ceil
from typing import List, Optional, Set, Tuple
import pydash
......@@ -33,15 +35,12 @@ def supremal_sublanguage(
mode: Mode = Mode.CONTROLLABLE_NORMAL,
preprocess: bool = True,
prefix_closed: bool = False,
num_cores: int = None,
num_cores: int = 1,
) -> DFA:
"""
Computes the supremal controllable and/or normal supervisor for the given plant and specification Automata.
"""
if not num_cores:
MAX_PROCESSES = 1
else:
MAX_PROCESSES = max(cpu_count(), num_cores)
max_processses = min(cpu_count(), num_cores)
G_given = plant.copy()
if not isinstance(spec, DFA) and not isinstance(spec, set):
......@@ -89,13 +88,13 @@ def supremal_sublanguage(
while True:
deleted_states = set()
if mode in [Mode.NORMAL, Mode.CONTROLLABLE_NORMAL]:
bad_states_for_normality = check_normality(H, G_obs_names, MAX_PROCESSES)
bad_states_for_normality = check_normality(H, G_obs_names, max_processses)
H.delete_vertices(bad_states_for_normality)
deleted_states |= bad_states_for_normality
if mode in [Mode.CONTROLLABLE, Mode.CONTROLLABLE_NORMAL]:
inacc_states = unary.find_inacc(H)
H.delete_vertices(inacc_states)
bad_states_for_controllability = check_controllability(H, G, MAX_PROCESSES)
bad_states_for_controllability = check_controllability(H, G, max_processses)
H.delete_vertices(bad_states_for_controllability)
deleted_states |= inacc_states | bad_states_for_controllability
......@@ -113,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: DFA, max_processes: int) -> StateSet:
"""
Check the normality condition of states H and returns states violating the condition.
"""
......@@ -122,15 +121,17 @@ def check_normality(H: DFA, G_obs_names: DFA, MAX_PROCESSES: int) -> StateSet:
bad_states = set()
all_H_names = H.vs["name"]
with ProcessPoolExecutor(max_workers=MAX_PROCESSES) as executor:
with ProcessPoolExecutor(mp_context=mp.get_context('fork'),max_workers=max_processes) as executor:
futures = []
chk = H.vcount() // MAX_PROCESSES
for i, H_indecies in enumerate(
pydash.chunk(range(H.vcount()), chk if chk > 0 else H.vcount(),)
):
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
__find_bad_states_normal,
H_indecies,
G_obs_names,
all_H_names,
i + 1,
)
)
......@@ -154,14 +155,14 @@ def __find_bad_states_normal(
):
y = H_names[index]
for q in G_obs_names:
if y in q and not q <= set(H_names):
if y in q and not set(q) <= set(H_names):
bad_states.add(index)
break
return bad_states
def check_controllability(H: DFA, G: DFA, MAX_PROCESSES: int) -> StateSet:
def check_controllability(H: DFA, G: DFA, max_processes: int) -> StateSet:
"""
Check the controllability condition of states in H and returns states violating the condition.
"""
......@@ -175,14 +176,10 @@ def check_controllability(H: DFA, G: DFA, MAX_PROCESSES: int) -> StateSet:
bad_states = set()
Euc = G.Euc
with ProcessPoolExecutor(max_workers=MAX_PROCESSES) as executor:
with ProcessPoolExecutor(mp_context=mp.get_context('fork'),max_workers=max_processes) as executor:
futures = []
chk = len(H_all_states) // MAX_PROCESSES
for i, H_names in enumerate(
pydash.chunk(
list(H_all_states.keys()), chk if chk > 0 else len(H_all_states),
)
):
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,
......@@ -190,7 +187,7 @@ def check_controllability(H: DFA, G: DFA, MAX_PROCESSES: int) -> StateSet:
H_all_states,
G_all_states,
Euc,
i,
i + 1,
)
)
......
This diff is collapsed.
[tool.poetry]
name = "DESops"
version = "20.6.1a4"
version = "20.9.2"
description = ""
authors = ["Jack Weitze <jweitze@umich.edu>", "Romulo Meira Goes <r.meiragoes@gmail.com>", "Shoma Matsui <smatsui@umich.edu>"]
packages = [
......@@ -8,7 +8,7 @@ packages = [
]
[tool.poetry.dependencies]
python = "^3.8"
python = "^3.7"
python-igraph = "^0.8.0"
pycairo = {version="^1.19.1", optional=true}
pydash = "^4.7.6"
......
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