Author: karstenwolf
Date: Sun Jun 1 10:20:33 2014
New Revision: 9481
URL: http://svn.gna.org/viewcvs/service-tech?rev=9481&view=rev
Log:
Deadlock as atomic proposition:
updated stubborn set generation for state predicate and tscc
Modified:
trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.cc
trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.h
trunk/lola2/src/Exploration/FirelistStubbornTscc.cc
trunk/lola2/src/Exploration/FirelistStubbornTscc.h
Modified: trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.cc?rev=9481&r1=9480&r2=9481&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.cc
(original)
+++ trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.cc Sun Jun
1 10:20:33 2014
@@ -8,6 +8,7 @@
#include <Exploration/Firelist.h>
#include <Exploration/FirelistStubbornStatePredicate.h>
+#include <Exploration/FirelistStubbornDeadlock.h>
#include <Exploration/StatePredicateProperty.h>
#include <Formula/StatePredicate/StatePredicate.h>
#include <Net/Net.h>
@@ -18,7 +19,7 @@
#include <cstdio>
FirelistStubbornStatePredicate::FirelistStubbornStatePredicate(StatePredicate
*p) :
- predicate(p), dfsStack(new index_t[Net::Card[TR]]), onStack(new
bool[Net::Card[TR]]())
+ predicate(p), dfsStack(new index_t[Net::Card[TR]]), onStack(new
bool[Net::Card[TR]]()),dl(new FirelistStubbornDeadlock())
{}
FirelistStubbornStatePredicate::~FirelistStubbornStatePredicate()
@@ -67,18 +68,31 @@
}
}
}
- index_t size = cardEnabled;
- * result = new index_t [cardEnabled];
- for (index_t i = 0; i < stackpointer; ++i)
+ if(cardEnabled || ! needEnabled)
{
- const index_t t = dfsStack[i];
- if (ns.Enabled[t])
+ // if up set for deadlock AP is required but there is an enabled
+ // transition so far, this enabled transition serves as a valid
+ // up set
+ index_t size = cardEnabled;
+ * result = new index_t [cardEnabled];
+ for (index_t i = 0; i < stackpointer; ++i)
{
- (*result)[--cardEnabled] = t;
+ const index_t t = dfsStack[i];
+ if (ns.Enabled[t])
+ {
+ (*result)[--cardEnabled] = t;
+ }
+ onStack[t] = false;
}
- onStack[t] = false;
+ return size;
}
- return size;
+ else
+ {
+ // if no enabled transition is in the stubborn set bit an up set
+ // for deadlock is required, we return a deadlock preserving
+ // up set.
+ return dl->getFirelist(ns,result);
+ }
}
Firelist *FirelistStubbornStatePredicate::createNewFireList(SimpleProperty
*property)
Modified: trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.h
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.h?rev=9481&r1=9480&r2=9481&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.h
(original)
+++ trunk/lola2/src/Exploration/FirelistStubbornStatePredicate.h Sun Jun
1 10:20:33 2014
@@ -9,6 +9,7 @@
#pragma once
#include <Core/Dimensions.h>
+#include <Exploration/FirelistStubbornDeadlock.h>
class Firelist;
class StatePredicate;
@@ -30,4 +31,5 @@
StatePredicate *predicate;
index_t *dfsStack;
bool *onStack;
+ FirelistStubbornDeadlock * dl;
};
Modified: trunk/lola2/src/Exploration/FirelistStubbornTscc.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/FirelistStubbornTscc.cc?rev=9481&r1=9480&r2=9481&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/FirelistStubbornTscc.cc (original)
+++ trunk/lola2/src/Exploration/FirelistStubbornTscc.cc Sun Jun 1 10:20:33 2014
@@ -8,6 +8,7 @@
#include <Exploration/Firelist.h>
#include <Exploration/FirelistStubbornTscc.h>
+#include <Exploration/FirelistStubbornDeadlock.h>
#include <Net/Net.h>
#include <Net/NetState.h>
#include <Net/Transition.h>
@@ -22,7 +23,8 @@
FirelistStubbornTscc::FirelistStubbornTscc(SimpleProperty *simpleproperty) :
sp(static_cast<StatePredicateProperty *>(simpleproperty)),
dfsStack(new index_t[Net::Card[TR]]),
- onStack(new bool[Net::Card[TR]]())
+ onStack(new bool[Net::Card[TR]]()),
+ dl(new FirelistStubbornDeadlock())
{}
FirelistStubbornTscc::~FirelistStubbornTscc()
@@ -110,18 +112,32 @@
}
}
}
- index_t size = cardEnabled;
- * result = new index_t [cardEnabled];
- for (index_t i = 0; i < stackpointer; ++i)
+ if(cardEnabled || !needEnabled)
{
- const index_t t = dfsStack[i];
- if (ns.Enabled[t])
- {
- (*result)[--cardEnabled] = t;
- }
- onStack[t] = false;
+ // an up set for deadlock atomic propositions is any
+ // enabled transition. If, through the other up sets,
+ // an eabled transition is there, everything is ok.
+ index_t size = cardEnabled;
+ * result = new index_t [cardEnabled];
+ for (index_t i = 0; i < stackpointer; ++i)
+ {
+ const index_t t = dfsStack[i];
+ if (ns.Enabled[t])
+ {
+ (*result)[--cardEnabled] = t;
+ }
+ onStack[t] = false;
+ }
+ return size;
}
- return size;
+ else
+ {
+ // If the other up sets to not yield an enabled transition,
+ // we need to return a stubborn set with an enabled
+ // transition. This is exactly any deadlock preserving
+ // stubborn set.
+ return dl -> getFirelist(ns,result);
+ }
}
Modified: trunk/lola2/src/Exploration/FirelistStubbornTscc.h
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/FirelistStubbornTscc.h?rev=9481&r1=9480&r2=9481&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/FirelistStubbornTscc.h (original)
+++ trunk/lola2/src/Exploration/FirelistStubbornTscc.h Sun Jun 1 10:20:33 2014
@@ -10,6 +10,7 @@
#pragma once
#include <Core/Dimensions.h>
+#include <Exploration/FirelistStubbornDeadlock.h>
class Firelist;
class StatePredicateProperty;
@@ -30,5 +31,6 @@
virtual index_t getFirelist(NetState &ns, index_t **);
virtual Firelist *createNewFireList(SimpleProperty *property);
+ FirelistStubbornDeadlock * dl;
};
--
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.
