Author: karstenwolf
Date: Tue Jun 3 17:33:23 2014
New Revision: 9486
URL: http://svn.gna.org/viewcvs/service-tech?rev=9486&view=rev
Log:
The new files
Added:
trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.cc
trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.h
Added: trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.cc?rev=9486&view=auto
==============================================================================
--- trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.cc (added)
+++ trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.cc Tue Jun 3
17:33:23 2014
@@ -0,0 +1,191 @@
+/*!
+\file AtomicStatePredicate.cc
+\author Karsten
+\status new
+
+\brief class implementation for deadlock state predicates
+*/
+
+#include <config.h>
+#include <Formula/StatePredicate/DeadlockPredicate.h>
+#include <Net/Net.h>
+#include <Net/Place.h>
+#include <Net/NetState.h>
+#include <Net/Marking.h>
+#include <CoverGraph/CoverGraph.h>
+#include <Formula/FormulaInfo.h>
+
+#include <cstdlib>
+#include <iostream>
+
+/*!
+\brief creates a state predicate with a formal sum of p places with positive
+factor, n places with negative factor, and constant k particular places are
+added using addPos and addNeg
+
+\param p number of places with positive factor
+\param n number of places with negative factor
+\param k constant
+
+\todo Schleifen behandeln - können evtl. rausgenommen werden
+*/
+DeadlockPredicate::DeadlockPredicate(bool ssign) :
+ sign(ssign)
+{
+}
+
+DeadlockPredicate::~DeadlockPredicate()
+{
+}
+
+
+/*!
+\brief participate in finding an upset: for deadlock: set need_enabled to
true; for no_deadlock: return empty set
+
+\param stack transitions found so far (irrelevant for us)
+\param onstack array where included transitions are marked (irrelevant for us)
+\param need_enabled reference parameter that signals that final up-set needs
to contain an enabled transition
+\return number of elements on stack
+*/
+index_t DeadlockPredicate::getUpSet(index_t *stack, bool *onstack, bool *
need_enabled) const
+{
+ if(sign)
+ {
+ // property is deadlock
+ *need_enabled = true;
+ }
+ else
+ {
+ // property is no deadlock
+ *need_enabled = false;
+ }
+ return 0;
+}
+
+/*!
+If value of this changes, it needs to be propagated to its parent. The
+parameter is the change in the formal sum k_1 p_1 + ... + k_n p_n between the
+previously considered marking and the current marking. Having a precomputed
+value for this change, evaluation of the formula is accelerated.
+*/
+void DeadlockPredicate::update(NetState& ns)
+{
+ bool newvalue = (sign ? ns.CardEnabled == 0 : ns.CardEnabled != 0);
+ if(parent)
+ {
+ if(newvalue && ! value)
+ {
+ value = newvalue;
+ parent->updateFT(position);
+ return;
+ }
+ if(!newvalue && value)
+ {
+ parent -> updateTF(position);
+ }
+
+ }
+ value = newvalue;
+}
+
+/*!
+Evaluation starts top/down, so the whole formula is examined. Evaluation is
+done w.r.t. ns.Current.
+
+\param ns net state to evaluate the formula
+*/
+void DeadlockPredicate::evaluate(NetState &ns)
+{
+ value = sign ? ns.CardEnabled == 0 : ns.CardEnabled != 0;
+}
+
+/*!
+Evaluation with Omega starts top/down, so the whole formula is examined.
Evaluation is
+done w.r.t. ns.Current.
+
+\param ns net state to evaluate the formula
+*/
+void DeadlockPredicate::evaluateOmega(NetState &ns)
+{
+ unknown = false;
+ value = sign ? ns.CardEnabled == 0 : ns.CardEnabled != 0;
+ if(ns.CardEnabled != 0)
+ {
+ for(index_t i = 0; i < Place::CardSignificant; i++)
+ {
+ if(ns.Current[i] == OMEGA)
+ {
+ unknown = true;
+ }
+
+ }
+ }
+}
+
+index_t DeadlockPredicate::countAtomic() const
+{
+ return 0;
+}
+
+index_t DeadlockPredicate::collectAtomic(AtomicStatePredicate **c)
+{
+ return 0;
+}
+
+index_t DeadlockPredicate::countDeadlock() const
+{
+ return 1;
+}
+
+index_t DeadlockPredicate::collectDeadlock(DeadlockPredicate **c)
+{
+ c[0] = this;
+ return 1;
+}
+
+// LCOV_EXCL_START
+bool DeadlockPredicate::DEBUG__consistency(NetState &ns)
+{
+ return true;
+}
+// LCOV_EXCL_STOP
+
+/*!
+\param parent the parent predicate for the new, copied, object
+*/
+StatePredicate *DeadlockPredicate::copy(StatePredicate *parent)
+{
+ DeadlockPredicate *af = new DeadlockPredicate(sign);
+ af->value = value;
+ af->position = position;
+ af->parent = parent;
+ return af;
+}
+
+index_t DeadlockPredicate::getSubs(__attribute__((__unused__))const
StatePredicate *const **subs)
+const
+{
+ return 0;
+}
+
+StatePredicate *DeadlockPredicate::negate()
+{
+ DeadlockPredicate *af = new DeadlockPredicate(!sign);
+ return af;
+}
+
+FormulaInfo *DeadlockPredicate::getInfo() const
+{
+ FormulaInfo *Info = new FormulaInfo();
+ if(sign) Info->tag = formula_deadlock;
+ else Info->tag= formula_nodeadlock;
+ Info->cardChildren = 0;
+ Info->f = NULL;
+ return Info;
+}
+
+int DeadlockPredicate::countSubFormulas() const
+{
+ return 1;
+}
+
Added: trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.h
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.h?rev=9486&view=auto
==============================================================================
--- trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.h (added)
+++ trunk/lola2/src/Formula/StatePredicate/DeadlockPredicate.h Tue Jun 3
17:33:23 2014
@@ -0,0 +1,77 @@
+/*!
+\file
+\author Karsten
+\status new
+
+\brief class definition for deadlocks as atomic state predicates
+*/
+
+#pragma once
+
+#include <Formula/StatePredicate/StatePredicate.h>
+
+/*!
+A state predicate is a formula that assigns a Boolean value to Marking::Current
+An atomic predicate compares a formal sum of places with a constant The general
+shape is: \f$ k_1 \cdot p_1 + \cdots + k_n \cdot p_n \leq k \f$
+*/
+class DeadlockPredicate : public StatePredicate
+{
+public:
+ DeadlockPredicate(bool); // arg: true = deadlock, false = !deadlock
+
+ ~DeadlockPredicate();
+
+ /// updates the value of this sub formula
+ void update(NetState &ns);
+
+ /// evaluates a formula, e.g. upon initialization
+ virtual void evaluate(NetState &ns);
+
+ /// evaluates a formula including omega values
+ virtual void evaluateOmega(NetState &ns);
+
+ /// participate in finding an up-set:
+ virtual index_t getUpSet(index_t *, bool *, bool *) const;
+
+ /// returns the negated version of this property, but leaves the current
one untouched
+ virtual StatePredicate *negate();
+
+ /// returns info on a particular node in the formula tree
+ FormulaInfo *getInfo() const;
+ /// returns the number of subformulas
+ int countSubFormulas() const;
+
+private:
+ /// updates the value of the predicate from true to false
+ void updateTF(index_t) {} // LCOV_EXCL_LINE
+
+ /// updates the value of the predicate from false to true
+ void updateFT(index_t) {} // LCOV_EXCL_LINE
+
+ bool DEBUG__consistency(NetState &ns);
+
+ /// direct read access for the deletion algorithm
+ index_t getSubs(const StatePredicate *const **subs) const;
+
+public:
+
+ bool sign; // true = property is "deadlock", false = property is "no
deadlock"
+
+ /// counts atomic subformulas
+ index_t countAtomic() const;
+
+ /// collects atomic subformulas; array must be malloced beforehand
+ /// result is number of inserted elements
+ index_t collectAtomic(AtomicStatePredicate **);
+
+ /// counts deadlock subformulas
+ index_t countDeadlock() const;
+
+ /// collects deadlock subformulas; array must be malloced beforehand
+ /// result is number of inserted elements
+ index_t collectDeadlock(DeadlockPredicate **);
+
+ // copy function
+ StatePredicate *copy(StatePredicate *parent);
+};
--
You received this e-mail, because you subscribed the mailing list
"service-tech-commits" which will forward you any e-mail addressed to
[email protected]. If you want to unsubscribe or make any changes to
your subscription, please go to
https://mail.gna.org/listinfo/service-tech-commits.
