DiaDes  0.1
DIAgnosis of Discrete-Event System
Macros | Functions
Assertion.hh File Reference
#include <string>
#include <stdexcept>
#include <boost/format.hpp>
#include <diades/utils/Verbose.hh>
#include <diades/utils/Exceptions.hh>

Go to the source code of this file.

Macros

#define require(Exception, expr, message)   ;
 
#define ensure(Exception, expr, message)   ;
 
#define assertion(Exception, expr, message)   ;
 
#define debug(x)   ;
 
#define always_require(Exception, expr, message)   Require<Exception>(expr,message)
 
#define always_ensure(Exception, expr, message)   Ensure<Exception>(expr,message)
 
#define always_assertion(Exception, expr, message)   Assertion<Exception>(expr,message)
 

Functions

template<class X , class A >
void Require (A assertion, const string &s)
 
template<class X , class A >
void Require (A assertion, const Diades::Utils::Msg &fmt)
 
template<class X , class A >
void Ensure (A assertion, const string &s)
 
template<class X , class A >
void Ensure (A assertion, const Diades::Utils::Msg &fmt)
 
template<class X , class A >
void Assertion (A assertion, const string &s)
 
template<class X , class A >
void Assertion (A assertion, const Diades::Utils::Msg &fmt)
 

Detailed Description

File defining the properties checking procedures. If a procedure fails the check then it sends an exception.

Definition in file Assertion.hh.

Macro Definition Documentation

◆ always_assertion

#define always_assertion (   Exception,
  expr,
  message 
)    Assertion<Exception>(expr,message)

Definition at line 124 of file Assertion.hh.

Referenced by generateSharedEvents(), and main().

◆ always_ensure

#define always_ensure (   Exception,
  expr,
  message 
)    Ensure<Exception>(expr,message)

Definition at line 123 of file Assertion.hh.

Referenced by getOutputProjection().

◆ always_require

#define always_require (   Exception,
  expr,
  message 
)    Require<Exception>(expr,message)

◆ assertion

#define assertion (   Exception,
  expr,
  message 
)    ;

◆ debug

#define debug (   x)    ;

Definition at line 118 of file Assertion.hh.

Referenced by generateBehaviour(), getSynchronisedInteraction(), and main().

◆ ensure

#define ensure (   Exception,
  expr,
  message 
)    ;

Definition at line 98 of file Assertion.hh.

Referenced by Diades::Automata::Experimental::SynchronisationEvent< StateMachine >::addEvent(), Diades::Automata::Topology::addNode(), Diades::Graph::Edge::changeSource(), Diades::Graph::Edge::changeTarget(), Diades::Automata::Experimental::ParametrizedSynchronisation< StateMachine >::close(), Diades::Automata::FaultDiagnosis::componentDiagnose(), Diades::Graph::ConstEdgeMap< ValueType >::ConstEdgeMap(), Diades::Graph::ConstNodeMap< set< Diades::Automata::Event > >::ConstNodeMap(), Diades::Graph::Edge::create(), Diades::Graph::Node::create(), Diades::Graph::Edge::destroy(), Diades::Graph::Node::destroy(), Diades::Graph::EdgeMap< Diades::Automata::FaultPattern::EventOccurrence >::EdgeMap(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::eraseEventPropertyId(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::finaliseStatePropertyIds(), generateComponent(), generateTransitionSystem(), generateTriggerableEvents(), Diades::Automata::Component::getEvent(), Diades::Automata::Experimental::SynchronisationRules< StateMachine >::getSynchronisationEvents(), Diades::Automata::FaultDiagnosis::globalModelDiagnose(), Diades::Graph::GraphIterator< Edge >::GraphIterator(), Diades::Graph::EdgeMap< Diades::Automata::FaultPattern::EventOccurrence >::init(), Diades::Graph::ConstNodeMap< set< Diades::Automata::Event > >::init(), Diades::Graph::NodeMap< Status >::init(), Diades::Graph::ConstEdgeMap< ValueType >::init(), Diades::Graph::ConstNodeMap< set< Diades::Automata::Event > >::initValue(), Diades::Graph::NodeMap< Status >::initValue(), Diades::Graph::ConstEdgeMap< ValueType >::initValue(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::insertEventPropertyId(), Diades::Sdmdl::Rule::makeEffect(), Diades::Sdmdl::Rule::makePrecondition(), Diades::Automata::Component::name(), Diades::Petri::BoundedNet::name(), Diades::Petri::BoundedNet::newPlace(), Diades::Petri::Net::newPlace(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::newState(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::newTransition(), Diades::Graph::NodeMap< Status >::NodeMap(), Diades::Graph::GraphIterator< Edge >::operator++(), Diades::Graph::EdgeMap< Diades::Automata::FaultPattern::EventOccurrence >::operator[](), Diades::Graph::ConstNodeMap< set< Diades::Automata::Event > >::operator[](), Diades::Graph::NodeMap< Status >::operator[](), Diades::Graph::ConstEdgeMap< ValueType >::operator[](), Diades::Automata::Component::setName(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::setStatePropertyId(), Diades::Automata::Experimental::SynchronisationEvent< StateMachine >::SynchronisationEvent(), Diades::Automata::Experimental::ParametrizedSynchronisation< StateMachine >::synchronise(), and Diades::Automata::SynchronisationEvent::synchronisedEvent().

◆ require

#define require (   Exception,
  expr,
  message 
)    ;

Definition at line 90 of file Assertion.hh.

Referenced by Diades::Automata::Experimental::SynchronisationEvent< StateMachine >::addEvent(), Diades::Petri::ReachabilityGraph::addMarking(), Diades::Petri::BoundedNet::addPost(), Diades::Petri::BoundedNet::addPre(), Diades::Petri::TimeReachabilityGraph::addTimeConstraint(), Diades::Sdmdl::Variable::assign(), Diades::Sdmdl::FormulaFactory::bddManager(), Diades::Automata::Component::beginOfSourceStateOfEvent(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::beginOfSourceStateOfEvent(), Diades::Automata::ObservableComponent::beginOfSourceStateOfObservableEvent(), Diades::Automata::Component::beginOfTargetStateOfEvent(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::beginOfTargetStateOfEvent(), Diades::Automata::ObservableComponent::beginOfTargetStateOfObservableEvent(), Diades::Petri::LabelledNet::beginOfTransitionWithEvent(), Diades::Petri::Net::beginOfTransitionWithEvent(), Diades::Graph::Node::changeId(), Diades::Graph::Edge::changeSource(), Diades::Graph::Edge::changeTarget(), Diades::Graph::Graph::clear(), Diades::Automata::Topology::cliqueBegin(), Diades::Automata::Topology::cliqueEnd(), Diades::Automata::Experimental::ParametrizedSynchronisation< StateMachine >::close(), Diades::Automata::Experimental::EventSetManager< EventInfo, EventId >::code(), Diades::Petri::TimeReachabilityGraph::constraintBegin(), Diades::Petri::TimeReachabilityGraph::constraintEnd(), Diades::Automata::Experimental::EventSetManager< EventInfo, EventId >::contains(), Diades::Automata::Topology::contains(), Diades::Automata::Component::containsEvent(), Diades::Automata::ObservableComponent::containsObservableEvent(), Diades::Graph::Edge::create(), Diades::Graph::Node::create(), Diades::Sdmdl::CubeGenerator::CubeGenerator(), Diades::Graph::Graph::cycleDetection(), Diades::Graph::Node::degree(), Diades::Graph::Graph::deleteAllEdges(), Diades::Graph::Graph::deleteEdge(), Diades::Graph::Graph::deleteNode(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::deleteState(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::deleteTransition(), Diades::Graph::NodeData::delInEdge(), Diades::Graph::NodeData::delOutEdge(), Diades::Graph::Edge::destroy(), Diades::Graph::Node::destroy(), Diades::Automata::Experimental::determine(), Diades::Graph::Edge::Edge(), Diades::Graph::Graph::edgeBegin(), Diades::Graph::Graph::edgeCapacity(), Diades::Graph::Graph::edgeEnd(), Diades::Sdmdl::Rule::effect(), Diades::Graph::Graph::empty(), Diades::Automata::Component::endOfSourceStateOfEvent(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::endOfSourceStateOfEvent(), Diades::Automata::ObservableComponent::endOfSourceStateOfObservableEvent(), Diades::Automata::Component::endOfTargetStateOfEvent(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::endOfTargetStateOfEvent(), Diades::Automata::ObservableComponent::endOfTargetStateOfObservableEvent(), Diades::Petri::LabelledNet::endOfTransitionWithEvent(), Diades::Petri::Net::endOfTransitionWithEvent(), Diades::Automata::Experimental::EventSetManager< EventInfo, EventId >::event(), Diades::Automata::Experimental::EventSetManager< EventInfo, EventId >::eventSet(), Diades::Automata::Component::eventTransitionBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::eventTransitionBegin(), Diades::Automata::Component::eventTransitionEnd(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::eventTransitionEnd(), Diades::Sdmdl::BddComponent::factory(), Diades::Sdmdl::Experimental::BddStateMachine::factory(), Diades::Automata::FaultDiagnosis::FaultDiagnosis(), Diades::Graph::GraphNodeSet::findNode(), generateComponent(), generateTriggerableEvents(), Diades::Automata::SynchronisationEvent::getAssociatedEvent(), Diades::Automata::Experimental::SynchronisationEvent< StateMachine >::getAssociatedEvent(), Diades::Automata::TopologyMap::getComponent(), Diades::Sdmdl::BddModel::getComponent(), Diades::Automata::Experimental::SynchronisationRules< StateMachine >::getComponent(), Diades::Automata::SynchronisationRules::getComponent(), Diades::Automata::Topology::getConnectionLabel(), Diades::Automata::FaultDiagnosis::getDiagnosis(), Diades::Petri::LabelledNet::getEvent(), Diades::Automata::Component::getEvent(), Diades::Petri::Net::getEvent(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::getEvent(), Diades::Petri::ReachabilityGraph::getId(), Diades::Graph::NodeElement< T >::getInfo(), Diades::Sdmdl::UnfoldingStateTable< T >::getInfo(), Diades::Petri::Net::getInfoLabel(), Diades::Petri::ReachabilityGraph::getLabel(), Diades::Automata::Component::getLabel(), Diades::Petri::ReachabilityGraph::getMarking(), Diades::Automata::Topology::getNodeName(), Diades::Automata::Component::getState(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::getStatePropertyId(), Diades::Automata::Experimental::SynchronisationRules< StateMachine >::getSynchronisationEvents(), Diades::Graph::Edge::id(), Diades::Automata::Event::id(), Diades::Graph::Node::id(), Diades::Graph::Node::inDeg(), Diades::Graph::Node::inEdgeBegin(), Diades::Graph::Graph::inEdgeBegin(), Diades::Graph::Node::inEdgeEnd(), Diades::Graph::Graph::inEdgeEnd(), Diades::Petri::BoundedNet::inhibits(), Diades::Utils::InfoManager< std::string, size_t, NullValue< std::string >, NullValue< size_t >, std::hash< std::string > >::initialise(), Diades::Sdmdl::BddComponent::initialStates(), Diades::Sdmdl::Experimental::BddStateMachine::initialStates(), Diades::Sdmdl::ComponentType::inputEvent(), Diades::Automata::ComposableModel::inputEventTransitionBegin(), Diades::Automata::Component::inputEventTransitionBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::inputEventTransitionBegin(), Diades::Automata::ComposableModel::inputEventTransitionEnd(), Diades::Automata::Component::inputEventTransitionEnd(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::inputEventTransitionEnd(), Diades::Automata::ObservableComponent::inputObservableTransitionBegin(), Diades::Automata::ObservableComponent::inputObservableTransitionEnd(), Diades::Sdmdl::ComponentType::inputPort(), Diades::Automata::Component::inputTransitionBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::inputTransitionBegin(), Diades::Automata::Component::inputTransitionEnd(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::inputTransitionEnd(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::insertEventPropertyId(), Diades::Sdmdl::UnfoldingStateTable< T >::insertIfNotFound(), Diades::Sdmdl::Rule::insertOutputEvent(), Diades::Automata::Trace::isAcceptor(), Diades::Automata::ObservableMask::isDetectable(), Diades::Automata::ObservableMask::isIdentifiable(), Diades::Petri::Net::isPostponable(), Diades::Automata::Topology::isSimple(), Diades::Petri::BoundedNet::labelOfPlace(), Diades::Sdmdl::Rule::makeEffect(), Diades::Sdmdl::Rule::makePrecondition(), Diades::Automata::SpecialisedActiveDiagnoser::nameOfObservable(), Diades::Petri::BoundedNet::nameOfPlace(), Diades::Petri::BoundedNet::nameOfTransition(), Diades::Petri::BoundedNet::nameOfTransition2Dot(), Diades::Petri::BoundedNet::net2TinaTransitionInterval(), Diades::Petri::BoundedNet::net2TinaTransitionName(), Diades::Graph::Graph::newEdge(), Diades::Graph::Graph::newNode(), Diades::Petri::Net::newPlace(), Diades::Petri::BoundedNet::newTransition(), Diades::Petri::Net::newTransition(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::newTransition(), Diades::Automata::Event::nickname(), Diades::Graph::Node::Node(), Diades::Graph::Graph::nodeBegin(), Diades::Graph::Graph::nodeCapacity(), Diades::Automata::Topology::nodeConnectionBegin(), Diades::Automata::Topology::nodeConnectionEnd(), Diades::Graph::NodeElement< T >::NodeElement(), Diades::Graph::Graph::nodeEnd(), Diades::Graph::Graph::numberOfEdges(), Diades::Graph::Graph::numberOfNodes(), Diades::Automata::ObservableComponent::observableTransitionBegin(), Diades::Automata::ObservableComponent::observableTransitionEnd(), Diades::Sdmdl::Value::operator<(), Diades::Automata::BeliefState::operator=(), Diades::Graph::EdgeMap< Diades::Automata::FaultPattern::EventOccurrence >::operator[](), Diades::Graph::ConstNodeMap< set< Diades::Automata::Event > >::operator[](), Diades::Graph::NodeMap< Status >::operator[](), Diades::Graph::ConstEdgeMap< ValueType >::operator[](), Diades::Graph::Node::outDeg(), Diades::Graph::Node::outEdgeBegin(), Diades::Graph::Graph::outEdgeBegin(), Diades::Graph::Node::outEdgeEnd(), Diades::Graph::Graph::outEdgeEnd(), Diades::Sdmdl::ComponentType::outputEvent(), Diades::Automata::ComposableModel::outputEventTransitionBegin(), Diades::Automata::Component::outputEventTransitionBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::outputEventTransitionBegin(), Diades::Automata::ComposableModel::outputEventTransitionEnd(), Diades::Automata::Component::outputEventTransitionEnd(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::outputEventTransitionEnd(), Diades::Automata::ObservableComponent::outputObservableTransitionBegin(), Diades::Automata::ObservableComponent::outputObservableTransitionEnd(), Diades::Sdmdl::ComponentType::outputPort(), Diades::Automata::ComposableModel::outputTransitionBegin(), Diades::Automata::Component::outputTransitionBegin(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::outputTransitionBegin(), Diades::Automata::ComposableModel::outputTransitionEnd(), Diades::Automata::Component::outputTransitionEnd(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::outputTransitionEnd(), Diades::Graph::NodeData::owner(), Diades::Graph::Edge::owner(), Diades::Graph::Node::owner(), Diades::Sdmdl::Port::Port(), Diades::Petri::BoundedNet::postBegin(), Diades::Petri::BoundedNet::postEnd(), Diades::Petri::BoundedNet::postTransBegin(), Diades::Petri::BoundedNet::postTransEnd(), Diades::Petri::BoundedNet::preBegin(), Diades::Sdmdl::Rule::precondition(), Diades::Petri::BoundedNet::preEnd(), Diades::Petri::BoundedNet::preTransBegin(), Diades::Petri::BoundedNet::preTransEnd(), Diades::Automata::Topology::removeConnection(), Diades::Automata::Event::save(), Diades::Automata::Trace::setAcceptor(), Diades::Automata::Topology::setConnectionLabel(), Diades::Sdmdl::Variable::setDefault(), Diades::Petri::Net::setEvent(), Diades::Automata::Experimental::FaultyEventStateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::setFaulty(), Diades::Automata::Component::setFaulty(), Diades::Petri::Net::setInfoLabel(), Diades::Petri::BoundedNet::setInhibition(), Diades::Petri::ReachabilityGraph::setInitial(), Diades::Sdmdl::Rule::setInputEvent(), Diades::Petri::BoundedNet::setLabelOfPlace(), Diades::Petri::Net::setLabelOfPlace(), Diades::Petri::Net::setLabelOfTransition(), Diades::Automata::Component::setName(), Diades::Petri::BoundedNet::setName(), Diades::Petri::Net::setName(), Diades::Petri::BoundedNet::setNameOfPlace(), Diades::Petri::BoundedNet::setNameOfTransition(), Diades::Automata::Topology::setNodeName(), Diades::Automata::Trace::setNonAcceptor(), Diades::Automata::Experimental::FaultyEventStateMachine< _StatePropertyId, _EventPropertyId, _NullStatePropertyId, _NullEventPropertyId >::setNormal(), Diades::Automata::Component::setNormal(), Diades::Sdmdl::Variable::setObservable(), Diades::Automata::Experimental::StateMachine< _StatePropertyId, _InputSymbolId, _NullStatePropertyId, _NullInputSymbolId >::setStatePropertyId(), Diades::Sdmdl::Variable::setUnObservable(), Diades::Graph::Graph::source(), Diades::Graph::Edge::sourcePos(), Diades::Graph::Graph::sourceRef(), Diades::Automata::SubConfiguration::SubConfiguration(), Diades::Automata::Experimental::SynchronisationEvent< StateMachine >::SynchronisationEvent(), Diades::Automata::Experimental::ParametrizedSynchronisation< StateMachine >::synchronise(), Diades::Automata::SynchronisationEvent::synchronisedEvent(), Diades::Graph::Graph::target(), Diades::Graph::Edge::targetPos(), Diades::Graph::Graph::targetRef(), Diades::Petri::BoundedNet::transitionOfName(), Diades::Sdmdl::BddComponent::transitions(), Diades::Sdmdl::Experimental::BddStateMachine::transitions(), Diades::Sdmdl::Event::type(), Diades::Petri::BoundedNet::unsetInhibition(), Diades::Sdmdl::Experimental::Assignment::value(), Diades::Sdmdl::ComponentType::variable(), Diades::Sdmdl::Experimental::Assignment::variable(), Diades::Petri::Vdd::Vdd(), and Diades::Petri::Zsl::Zsl().

Function Documentation

◆ Assertion() [1/2]

template<class X , class A >
void Assertion ( assertion,
const string &  s 
)
inline

Assertion

Parameters
assertionPredicate to check
smessage of the exception X

Produce an exception of type X if assertion is not true

Definition at line 71 of file Assertion.hh.

◆ Assertion() [2/2]

template<class X , class A >
void Assertion ( assertion,
const Diades::Utils::Msg fmt 
)
inline

Assertion

Parameters
assertionPredicate to check
smessage of the exception X

Produce an exception of type X if assertion is not true

Definition at line 81 of file Assertion.hh.

◆ Ensure() [1/2]

template<class X , class A >
void Ensure ( assertion,
const string &  s 
)
inline

Postcondition

Parameters
assertionPredicate to check
smessage of the exception X

Produce an exception of type X if assertion is not true

Definition at line 48 of file Assertion.hh.

◆ Ensure() [2/2]

template<class X , class A >
void Ensure ( assertion,
const Diades::Utils::Msg fmt 
)
inline

Postcondition

Parameters
assertionPredicate to check
smessage of the exception X

Produce an exception of type X if assertion is not true

Definition at line 60 of file Assertion.hh.

◆ Require() [1/2]

template<class X , class A >
void Require ( assertion,
const string &  s 
)
inline

Precondition

Parameters
assertionPredicate to check
smessage of the exception X

Produce an exception of type X if assertion is not true

Definition at line 28 of file Assertion.hh.

◆ Require() [2/2]

template<class X , class A >
void Require ( assertion,
const Diades::Utils::Msg fmt 
)
inline

Precondition

Parameters
assertionPredicate to check
smessage of the exception X

Produce an exception of type X if assertion is not true

Definition at line 38 of file Assertion.hh.