From 554b34afcfd8620ca63e4ebb37c7ba806051bd0b Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 10 Apr 2026 14:30:46 +0100 Subject: [PATCH] Refactoring: Python/SMT --- reactics-smt/rs/context_automaton.py | 12 ++--- .../context_automaton_with_concentrations.py | 9 ++-- reactics-smt/rs/extended_context_automaton.py | 2 +- reactics-smt/rs/reaction_system.py | 7 +-- .../rs/reaction_system_with_concentrations.py | 47 ++----------------- ...action_system_with_concentrations_param.py | 18 ++----- reactics-smt/rs_testing.py | 2 - reactics-smt/rssmt.py | 1 - reactics-smt/smt/__init__.py | 1 - reactics-smt/smt/smt_checker_rs.py | 2 +- reactics-smt/smt/smt_checker_rsc.py | 3 -- reactics-smt/smt/smt_checker_rsc_param.py | 3 -- 12 files changed, 20 insertions(+), 87 deletions(-) diff --git a/reactics-smt/rs/context_automaton.py b/reactics-smt/rs/context_automaton.py index 6d0a084..3b29e68 100644 --- a/reactics-smt/rs/context_automaton.py +++ b/reactics-smt/rs/context_automaton.py @@ -55,10 +55,7 @@ class ContextAutomaton(object): return self._states[self._init_state] def is_state(self, name): - if name in self._states: - return True - else: - return False + return name in self._states def get_state_id(self, name): try: @@ -78,10 +75,7 @@ class ContextAutomaton(object): print(state) def is_valid_rs_set(self, elements): - if set(elements).issubset(self._reaction_system.background_set): - return True - else: - return False + return set(elements).issubset(self._reaction_system.background_set) def is_valid_context(self, context): return self.is_valid_rs_set(context) @@ -95,7 +89,7 @@ class ContextAutomaton(object): return new_set def add_transition(self, src, context_set, dst): - if not type(context_set) is set and not type(context_set) is list: + if not isinstance(context_set, (set, list)): print("Contexts set must be of type set or list") if not self.is_valid_context(context_set): diff --git a/reactics-smt/rs/context_automaton_with_concentrations.py b/reactics-smt/rs/context_automaton_with_concentrations.py index 14b0271..f702df1 100644 --- a/reactics-smt/rs/context_automaton_with_concentrations.py +++ b/reactics-smt/rs/context_automaton_with_concentrations.py @@ -9,12 +9,9 @@ class ContextAutomatonWithConcentrations(ContextAutomaton): super(ContextAutomatonWithConcentrations, self).__init__(reaction_system) def is_valid_context(self, context): - if set([e for e, lvl in context]).issubset( + return set(e for e, lvl in context).issubset( self._reaction_system.background_set - ): - return True - else: - return False + ) def context2str(self, ctx): if len(ctx) == 0: @@ -26,7 +23,7 @@ class ContextAutomatonWithConcentrations(ContextAutomaton): return s def add_transition(self, src, context_set, dst): - if not type(context_set) is set and not type(context_set) is list: + if not isinstance(context_set, (set, list)): print("Contexts set must be of type set or list") if not self.is_valid_context(context_set): diff --git a/reactics-smt/rs/extended_context_automaton.py b/reactics-smt/rs/extended_context_automaton.py index bae9ce2..502cb77 100644 --- a/reactics-smt/rs/extended_context_automaton.py +++ b/reactics-smt/rs/extended_context_automaton.py @@ -70,7 +70,7 @@ class ExtendedContextAutomaton(ContextAutomaton): ctx_reactants, ctx_inhibitors, ctx_products = ctx_reaction - if not type(ctx_products) is set and not type(ctx_products) is list: + if not isinstance(ctx_products, (set, list)): print("Contexts set (context products) must be of type set or list") if not self.is_valid_rs_set(ctx_reactants): diff --git a/reactics-smt/rs/reaction_system.py b/reactics-smt/rs/reaction_system.py index ad10a9f..e1d55fc 100644 --- a/reactics-smt/rs/reaction_system.py +++ b/reactics-smt/rs/reaction_system.py @@ -43,11 +43,8 @@ class ReactionSystem(object): self.add_bg_set_entity(e) def is_in_background_set(self, entity): - """Checks if the given name is valid wrt the background set=""" - if entity in self.background_set: - return True - else: - return False + """Checks if the given name is valid wrt the background set""" + return entity in self.background_set def get_entity_id(self, name): try: diff --git a/reactics-smt/rs/reaction_system_with_concentrations.py b/reactics-smt/rs/reaction_system_with_concentrations.py index 9bdeb28..00967c8 100644 --- a/reactics-smt/rs/reaction_system_with_concentrations.py +++ b/reactics-smt/rs/reaction_system_with_concentrations.py @@ -18,9 +18,9 @@ class ReactionSystemWithConcentrations(ReactionSystem): def add_bg_set_entity(self, e): name = "" def_max_conc = -1 - if type(e) is tuple and len(e) == 2: + if isinstance(e, tuple) and len(e) == 2: name, def_max_conc = e - elif type(e) is str: + elif isinstance(e, str): name = e print("\nWARNING: no maximal concentration level specified for:", e, "\n") else: @@ -46,18 +46,10 @@ class ReactionSystemWithConcentrations(ReactionSystem): def is_valid_entity_with_concentration(self, e): """Sanity check for entities with concentration""" - if type(e) is tuple: - if len(e) == 2 and type(e[1]) is int: - return True + if isinstance(e, (tuple, list)) and len(e) == 2 and isinstance(e[1], int): + return True - if type(e) is list: - if len(e) == 2 and type(e[1]) is int: - return True - - print("FATAL. Invalid entity+concentration: {:s}".format(e)) - exit(1) - - return False + raise RuntimeError("Invalid entity+concentration: " + repr(e)) def get_state_ids(self, state): """Returns entities of the given state without levels""" @@ -415,33 +407,4 @@ class ReactionSystemWithConcentrations(ReactionSystem): return rs -class ReactionSystemWithAutomaton(object): - def __init__(self, reaction_system, context_automaton): - self.rs = reaction_system - self.ca = context_automaton - - def show(self, soft=False): - self.rs.show(soft) - self.ca.show() - - def is_with_concentrations(self): - if not isinstance(self.rs, ReactionSystemWithConcentrations): - return False - if not isinstance(self.ca, ContextAutomatonWithConcentrations): - return False - return True - - def sanity_check(self): - pass - - def get_ordinary_reaction_system_with_automaton(self): - if not self.is_with_concentrations(): - raise RuntimeError("Not RS/CA with concentrations") - - ors = self.rs.get_reaction_system() - oca = self.ca.get_automaton_with_flat_contexts(ors) - - return ReactionSystemWithAutomaton(ors, oca) - - # EOF diff --git a/reactics-smt/rs/reaction_system_with_concentrations_param.py b/reactics-smt/rs/reaction_system_with_concentrations_param.py index ab628dc..1e52492 100644 --- a/reactics-smt/rs/reaction_system_with_concentrations_param.py +++ b/reactics-smt/rs/reaction_system_with_concentrations_param.py @@ -34,9 +34,9 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): def add_bg_set_entity(self, e): name = "" def_max_conc = -1 - if type(e) is tuple and len(e) == 2: + if isinstance(e, tuple) and len(e) == 2: name, def_max_conc = e - elif type(e) is str: + elif isinstance(e, str): name = e print("\nWARNING: no maximal concentration level specified for:", e, "\n") else: @@ -80,18 +80,10 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): def is_valid_entity_with_concentration(self, e): """Sanity check for entities with concentration""" - if type(e) is tuple: - if len(e) == 2 and type(e[1]) is int: - return True + if isinstance(e, (tuple, list)) and len(e) == 2 and isinstance(e[1], int): + return True - if type(e) is list: - if len(e) == 2 and type(e[1]) is int: - return True - - print("FATAL. Invalid entity+concentration: {:s}".format(e)) - exit(1) - - return False + raise RuntimeError("Invalid entity+concentration: " + repr(e)) def is_valid_concentration_for_entity(self, entity, level): """Checks the concentration level for entity""" diff --git a/reactics-smt/rs_testing.py b/reactics-smt/rs_testing.py index 727dcce..c492227 100644 --- a/reactics-smt/rs_testing.py +++ b/reactics-smt/rs_testing.py @@ -1,12 +1,10 @@ from rs import * from smt import * -import rs_examples from logics import * from rsltl_shortcuts import * from itertools import chain, combinations -import sys import resource def powerset(iterable,N=None): diff --git a/reactics-smt/rssmt.py b/reactics-smt/rssmt.py index 4ebf902..95398ec 100755 --- a/reactics-smt/rssmt.py +++ b/reactics-smt/rssmt.py @@ -11,7 +11,6 @@ import argparse from rs import * from smt import * import sys -import rs_examples import rs_testing from colour import * diff --git a/reactics-smt/smt/__init__.py b/reactics-smt/smt/__init__.py index dbce176..af9a852 100644 --- a/reactics-smt/smt/__init__.py +++ b/reactics-smt/smt/__init__.py @@ -1,4 +1,3 @@ -# from smt.smt_checker import SmtChecker from smt.smt_checker_rs import SmtCheckerRS from smt.smt_checker_rsc import SmtCheckerRSC from smt.smt_checker_rsc_param import SmtCheckerRSCParam diff --git a/reactics-smt/smt/smt_checker_rs.py b/reactics-smt/smt/smt_checker_rs.py index 88242a4..57ee035 100644 --- a/reactics-smt/smt/smt_checker_rs.py +++ b/reactics-smt/smt/smt_checker_rs.py @@ -267,7 +267,7 @@ class SmtCheckerRS(object): ): """Main testing function""" - if not type(state) is tuple: + if not isinstance(state, tuple): state = (state, []) if print_time: diff --git a/reactics-smt/smt/smt_checker_rsc.py b/reactics-smt/smt/smt_checker_rsc.py index 9b4a795..7934e73 100644 --- a/reactics-smt/smt/smt_checker_rsc.py +++ b/reactics-smt/smt/smt_checker_rsc.py @@ -11,9 +11,6 @@ from colour import * from logics import rsLTL_Encoder -# def simplify(x): -# return x - class SmtCheckerRSC(object): def __init__(self, rsca): diff --git a/reactics-smt/smt/smt_checker_rsc_param.py b/reactics-smt/smt/smt_checker_rsc_param.py index 2d48fcf..c345025 100644 --- a/reactics-smt/smt/smt_checker_rsc_param.py +++ b/reactics-smt/smt/smt_checker_rsc_param.py @@ -14,9 +14,6 @@ from logics import ParamConstr_Encoder from rs.reaction_system_with_concentrations_param import ParameterObj, is_param -# def simplify(x): -# return x - def z3_max(a, b): return If(a > b, a, b)