From 911d8dcf415204cfe938618459659c49499a007b Mon Sep 17 00:00:00 2001 From: TanguyDubois Date: Thu, 17 Oct 2024 14:10:22 +0200 Subject: [PATCH] Fixed inhibitors when no preset --- include/Core/TAPN/TimedTransition.hpp | 4 +++- src/DiscreteVerification/Generators/SMCRunGenerator.cpp | 4 ++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/include/Core/TAPN/TimedTransition.hpp b/include/Core/TAPN/TimedTransition.hpp index 6a961a00..6eed6504 100755 --- a/include/Core/TAPN/TimedTransition.hpp +++ b/include/Core/TAPN/TimedTransition.hpp @@ -68,7 +68,9 @@ namespace VerifyTAPN { inline unsigned int getNumberOfInputArcs() const { return preset.size(); }; - inline unsigned int getNumberOfTransportArcs() const { return transportArcs.size(); }; + inline unsigned int getNumberOfTransportArcs() const { return transportArcs.size(); } + + inline unsigned int getNumberOfInhibitorArcs() const { return inhibitorArcs.size(); } inline bool isConservative() const { return preset.size() == postset.size(); } diff --git a/src/DiscreteVerification/Generators/SMCRunGenerator.cpp b/src/DiscreteVerification/Generators/SMCRunGenerator.cpp index e8f20e64..d6378d94 100644 --- a/src/DiscreteVerification/Generators/SMCRunGenerator.cpp +++ b/src/DiscreteVerification/Generators/SMCRunGenerator.cpp @@ -25,7 +25,7 @@ namespace VerifyTAPN { double originMaxDelay = _origin->availableDelay(); std::vector> invInterval = { interval(0, originMaxDelay) }; for(auto transi : _tapn.getTransitions()) { - if(transi->getPresetSize() == 0) { + if(transi->getPresetSize() == 0 && transi->getNumberOfInhibitorArcs() == 0) { _defaultTransitionIntervals[transi->getIndex()] = invInterval; } else { std::vector> firingDates = transitionFiringDates(transi); @@ -87,7 +87,7 @@ namespace VerifyTAPN { bool deadlocked = true; for(auto transi : _tapn.getTransitions()) { int i = transi->getIndex(); - if(transi->getPresetSize() == 0) { + if(transi->getPresetSize() == 0 && transi->getNumberOfInhibitorArcs() == 0) { _transitionIntervals[i] = invInterval; } else { std::vector> firingDates = transitionFiringDates(transi);