Author: vm069
Date: Mon May 26 14:55:37 2014
New Revision: 9456
URL: http://svn.gna.org/viewcvs/service-tech?rev=9456&view=rev
Log:
renamed FirelistStubbornAgef,added AGAF Exploration
* modified Task.cc to start TSCCExploration for AGAF (needs to done right,
currently uses FormulaType CTL and checks for tscc flag)
* TSCCExplorationAGAF contains duplicated code which should get deduplicated
* renamed FirelistStubbornAgef to FirelistStubbornTscc
Added:
trunk/lola2/src/Exploration/FirelistStubbornTscc.cc
- copied, changed from r9454,
trunk/lola2/src/Exploration/FirelistStubbornAgef.cc
trunk/lola2/src/Exploration/FirelistStubbornTscc.h
- copied, changed from r9454,
trunk/lola2/src/Exploration/FirelistStubbornAgef.h
trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc
- copied, changed from r9454,
trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc
Removed:
trunk/lola2/src/Exploration/FirelistStubbornAgef.cc
trunk/lola2/src/Exploration/FirelistStubbornAgef.h
Modified:
trunk/lola2/src/Exploration/TSCCExploration.h
trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc
trunk/lola2/src/Makefile.am
trunk/lola2/src/Planning/Task.cc
Removed: trunk/lola2/src/Exploration/FirelistStubbornAgef.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/FirelistStubbornAgef.cc?rev=9455&view=auto
==============================================================================
--- trunk/lola2/src/Exploration/FirelistStubbornAgef.cc (original)
+++ trunk/lola2/src/Exploration/FirelistStubbornAgef.cc (removed)
@@ -1,132 +0,0 @@
-/*!
-\file
-\author Markus
-\status new
-
-\brief Class for firelist generation. Generates a firelist based on Stubborn
-sets created by upsets and downsets
-*/
-
-#include <Exploration/Firelist.h>
-#include <Exploration/FirelistStubbornAgef.h>
-#include <Net/Net.h>
-#include <Net/NetState.h>
-#include <Net/Transition.h>
-#include <Exploration/SimpleProperty.h>
-#include <Exploration/StatePredicateProperty.h>
-#include <Formula/StatePredicate/StatePredicate.h>
-
-#include <cstdlib>
-#include <cstdio>
-
-
-FirelistStubbornAgef::FirelistStubbornAgef(SimpleProperty * simpleproperty)
-{
- sp =(StatePredicateProperty *) simpleproperty;
- dfsStack = new index_t[Net::Card[TR]];
- onStack = new bool[Net::Card[TR]]();
- fprintf(stderr,"created FirelistStubbornAgef\n");
-}
-
-FirelistStubbornAgef::~FirelistStubbornAgef()
-{
- delete[] dfsStack;
- delete[] onStack;
-}
-
-
-/*!
- \param ns the net-state for which the firelist should be determined
- \param[in,out] result the actual fire list (contains the enabled transitions
for this netstate)
- \result number of elements in fire list
- */
-index_t FirelistStubbornAgef::getFirelist(NetState &ns, index_t **result)
-{
- //if property is true then upset is empty
- // other cases for upset calulation:
- // Property := State Property
- // M(p) := Marking (eg. ns)
- // k := the natural number defined by property that
- // creates a border to M(p)
- //
- //
- // Property == M(p) <= k : up(M)
- // Property == M(p) = k : up(M)
- // Property == M(p) >= k : up(M)
- // Property == M(p) != k : up(M)
- index_t cardEnabled = 0;
- index_t stackpointer=0;
- //get the upset
- if(!sp->getPredicate()->value){
- stackpointer = sp->getPredicate()->getUpSet(dfsStack, onStack);
- }
- else
- {
- //do bruteforce firelist or just set upset empty?
- //stackpointer = 0;
- // for now use bruteforce
- assert(ns.CardEnabled <= Net::Card[TR]);
-
- *result = new index_t[ns.CardEnabled];
- index_t i = 0;
- for (index_t t = 0; t < Net::Card[TR]; ++t)
- {
- if (ns.Enabled[t])
- {
- assert(i < ns.CardEnabled);
- (*result)[i++] = t;
- }
- }
- return ns.CardEnabled;
-
- }
-
- fprintf(stderr,"stackp: %d\n",stackpointer);
-
- // loop until all stack elements processed
- for (index_t firstunprocessed = 0; firstunprocessed < stackpointer;
++firstunprocessed)
- {
- index_t currenttransition = dfsStack[firstunprocessed];
- index_t *mustbeincluded;
- index_t cardmustbeincluded;
- if (ns.Enabled[currenttransition])
- {
- ++cardEnabled;
- mustbeincluded = Transition::Conflicting[currenttransition];
- cardmustbeincluded =
Transition::CardConflicting[currenttransition];
- }
- else
- {
- const index_t scapegoat = ns.Arc[TR][PRE][currenttransition][0];
- mustbeincluded = ns.Arc[PL][PRE][scapegoat];
- cardmustbeincluded = Net::CardArcs[PL][PRE][scapegoat];
- }
- for (index_t i = 0; i < cardmustbeincluded; ++i)
- {
- const index_t t = mustbeincluded[i];
- if (!onStack[t])
- {
- dfsStack[stackpointer++] = t;
- onStack[t] = true;
- }
- }
- }
- 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;
-}
-
-
-Firelist
*FirelistStubbornAgef::createNewFireList(__attribute__((__unused__))SimpleProperty
* property)
-{
- return new FirelistStubbornAgef(property);
-}
Removed: trunk/lola2/src/Exploration/FirelistStubbornAgef.h
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/FirelistStubbornAgef.h?rev=9455&view=auto
==============================================================================
--- trunk/lola2/src/Exploration/FirelistStubbornAgef.h (original)
+++ trunk/lola2/src/Exploration/FirelistStubbornAgef.h (removed)
@@ -1,34 +0,0 @@
-/*!
-\file
-\author Markus
-\status new
-
-\brief class for firelist generation. Default is firelist consisting of all
-enabled transitions.
-*/
-
-#pragma once
-
-#include <Core/Dimensions.h>
-
-class Firelist;
-class StatePredicateProperty;
-
-/// a stubborn firelist for the search for deadlocks
-class FirelistStubbornAgef : public Firelist
-
-{
-public:
- FirelistStubbornAgef(SimpleProperty * simpleproperty);
- ~FirelistStubbornAgef();
-
- StatePredicateProperty * sp;
- /// return value contains number of elements in fire list, argument is
reference
- index_t * dfsStack;
- bool * onStack;
- /// parameter for actual list
- virtual index_t getFirelist(NetState &ns, index_t **);
-
- virtual Firelist *createNewFireList(SimpleProperty * property);
-
-};
Copied: trunk/lola2/src/Exploration/FirelistStubbornTscc.cc (from r9454,
trunk/lola2/src/Exploration/FirelistStubbornAgef.cc)
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/FirelistStubbornTscc.cc?p2=trunk/lola2/src/Exploration/FirelistStubbornTscc.cc&p1=trunk/lola2/src/Exploration/FirelistStubbornAgef.cc&r1=9454&r2=9456&rev=9456&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/FirelistStubbornAgef.cc (original)
+++ trunk/lola2/src/Exploration/FirelistStubbornTscc.cc Mon May 26 14:55:37 2014
@@ -1,14 +1,13 @@
/*!
-\file
+\file FirelistStubbornTscc
\author Markus
\status new
-
\brief Class for firelist generation. Generates a firelist based on Stubborn
sets created by upsets and downsets
*/
#include <Exploration/Firelist.h>
-#include <Exploration/FirelistStubbornAgef.h>
+#include <Exploration/FirelistStubbornTscc.h>
#include <Net/Net.h>
#include <Net/NetState.h>
#include <Net/Transition.h>
@@ -20,15 +19,15 @@
#include <cstdio>
-FirelistStubbornAgef::FirelistStubbornAgef(SimpleProperty * simpleproperty)
+FirelistStubbornTscc::FirelistStubbornTscc(SimpleProperty * simpleproperty)
{
sp =(StatePredicateProperty *) simpleproperty;
dfsStack = new index_t[Net::Card[TR]];
onStack = new bool[Net::Card[TR]]();
- fprintf(stderr,"created FirelistStubbornAgef\n");
+ fprintf(stderr,"created FirelistStubbornTscc\n");
}
-FirelistStubbornAgef::~FirelistStubbornAgef()
+FirelistStubbornTscc::~FirelistStubbornTscc()
{
delete[] dfsStack;
delete[] onStack;
@@ -40,7 +39,7 @@
\param[in,out] result the actual fire list (contains the enabled transitions
for this netstate)
\result number of elements in fire list
*/
-index_t FirelistStubbornAgef::getFirelist(NetState &ns, index_t **result)
+index_t FirelistStubbornTscc::getFirelist(NetState &ns, index_t **result)
{
//if property is true then upset is empty
// other cases for upset calulation:
@@ -81,7 +80,7 @@
}
- fprintf(stderr,"stackp: %d\n",stackpointer);
+ //fprintf(stderr,"stackp: %d\n",stackpointer);
// loop until all stack elements processed
for (index_t firstunprocessed = 0; firstunprocessed < stackpointer;
++firstunprocessed)
@@ -126,7 +125,7 @@
}
-Firelist
*FirelistStubbornAgef::createNewFireList(__attribute__((__unused__))SimpleProperty
* property)
+Firelist
*FirelistStubbornTscc::createNewFireList(__attribute__((__unused__))SimpleProperty
* property)
{
- return new FirelistStubbornAgef(property);
+ return new FirelistStubbornTscc(property);
}
Copied: trunk/lola2/src/Exploration/FirelistStubbornTscc.h (from r9454,
trunk/lola2/src/Exploration/FirelistStubbornAgef.h)
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/FirelistStubbornTscc.h?p2=trunk/lola2/src/Exploration/FirelistStubbornTscc.h&p1=trunk/lola2/src/Exploration/FirelistStubbornAgef.h&r1=9454&r2=9456&rev=9456&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/FirelistStubbornAgef.h (original)
+++ trunk/lola2/src/Exploration/FirelistStubbornTscc.h Mon May 26 14:55:37 2014
@@ -15,12 +15,12 @@
class StatePredicateProperty;
/// a stubborn firelist for the search for deadlocks
-class FirelistStubbornAgef : public Firelist
+class FirelistStubbornTscc : public Firelist
{
public:
- FirelistStubbornAgef(SimpleProperty * simpleproperty);
- ~FirelistStubbornAgef();
+ FirelistStubbornTscc(SimpleProperty * simpleproperty);
+ ~FirelistStubbornTscc();
StatePredicateProperty * sp;
/// return value contains number of elements in fire list, argument is
reference
Modified: trunk/lola2/src/Exploration/TSCCExploration.h
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/TSCCExploration.h?rev=9456&r1=9455&r2=9456&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/TSCCExploration.h (original)
+++ trunk/lola2/src/Exploration/TSCCExploration.h Mon May 26 14:55:37 2014
@@ -46,3 +46,7 @@
bool depth_first(SimpleProperty &property, NetState &ns,
Store<statenumber_t> &myStore, Firelist &myFirelist, int threadNumber);
};
+class TSCCExplorationAGAF : public TSCCExploration
+{
+ bool depth_first(SimpleProperty &property, NetState &ns,
Store<statenumber_t> &myStore, Firelist &myFirelist, int threadNumber);
+};
Copied: trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc (from r9454,
trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc)
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc?p2=trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc&p1=trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc&r1=9454&r2=9456&rev=9456&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc (original)
+++ trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc Mon May 26 14:55:37 2014
@@ -1,5 +1,5 @@
/*!
-\file
+\file TSCCExplorationAGAF.cc
\author Markus
\status new
@@ -19,9 +19,11 @@
#include <climits>
-bool TSCCExplorationAGEF::depth_first(SimpleProperty &property, NetState
&ns,Store<statenumber_t> &myStore, Firelist &myFirelist,
__attribute__((__unused__))int threadNumber)
+bool TSCCExplorationAGAF::depth_first(SimpleProperty &property, NetState
&ns,Store<statenumber_t> &myStore, Firelist &myFirelist,
__attribute__((__unused__))int threadNumber)
{
- fprintf(stderr, "Tsccexplorationagef gets used\n");
+ fprintf(stderr, "Tsccexplorationagaf gets used\n");
+ //TODO this is mostly duplicated code of TSCCExplorationAGEF ... find a
+ //better way to do this
property.value = property.initProperty(ns);
Modified: trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc?rev=9456&r1=9455&r2=9456&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc (original)
+++ trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc Mon May 26 14:55:37 2014
@@ -139,7 +139,8 @@
}
else{
//there is a tscc in which the property is not true
- //then we can exit
+ //then we can exit going forward to find one path where it
+ //is true
return false;
}
//update the highest lowlink to the current
Modified: trunk/lola2/src/Makefile.am
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Makefile.am?rev=9456&r1=9455&r2=9456&view=diff
==============================================================================
--- trunk/lola2/src/Makefile.am (original)
+++ trunk/lola2/src/Makefile.am Mon May 26 14:55:37 2014
@@ -2,7 +2,7 @@
bin_PROGRAMS = lola
# increase stack size to 32 MB
-#lola_LDFLAGS = -Wl,-stack_size,0x2000000
+#lola_LDFLAGS = -pg
# the plain sources you need to compile (no generated code)
lola_SOURCES = $(KCSOURCES) \
@@ -25,6 +25,7 @@
Exploration/DFSExploration.cc
\
Exploration/TSCCExplorationAGEF.cc
\
Exploration/TSCCExplorationEFAGEF.cc
\
+ Exploration/TSCCExplorationAGAF.cc
\
Exploration/TSCCExploration.h
\
Exploration/DFSExploration.h
\
Exploration/DFSStackEntry.cc
\
@@ -33,8 +34,8 @@
Exploration/DeadlockExploration.h
\
Exploration/Firelist.cc
\
Exploration/Firelist.h
\
- Exploration/FirelistStubbornAgef.cc
\
- Exploration/FirelistStubbornAgef.h
\
+ Exploration/FirelistStubbornTscc.cc
\
+ Exploration/FirelistStubbornTscc.h
\
Exploration/FirelistStubbornDeadlock.cc \
Exploration/FirelistStubbornDeadlock.h
\
Exploration/FirelistStubbornDeletion.cc
\
Modified: trunk/lola2/src/Planning/Task.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Planning/Task.cc?rev=9456&r1=9455&r2=9456&view=diff
==============================================================================
--- trunk/lola2/src/Planning/Task.cc (original)
+++ trunk/lola2/src/Planning/Task.cc Mon May 26 14:55:37 2014
@@ -9,7 +9,7 @@
#include <Exploration/TSCCExploration.h>
#include <Exploration/Firelist.h>
#include <Exploration/FirelistStubbornDeadlock.h>
-#include <Exploration/FirelistStubbornAgef.h>
+#include <Exploration/FirelistStubbornTscc.h>
#include <Exploration/FirelistStubbornDeletion.h>
#include <Exploration/FirelistStubbornStatePredicate.h>
#include <Exploration/LTLExploration.h>
@@ -392,7 +392,7 @@
RT::rep->status("processing formula");
// simplify CTL formula to fewer operators
- if (formulaType == FORMULA_CTL)
+ if (formulaType == FORMULA_CTL && !RT::args.tscc_flag)
{
// replace path quantor+temporal operator by dedicated CTL operator
TheFormula = TheFormula->rewrite(kc::ctloperators);
@@ -420,6 +420,10 @@
break;
}
default:
+ if(RT::args.tscc_flag)
+ {
+ TheFormula = TheFormula->rewrite(kc::booleanlists);
+ }
break;
}
@@ -469,10 +473,23 @@
case FORMULA_CTL:
{
- TheFormula->unparse(myprinter, kc::ctl);
- ctlFormula = TheFormula->ctl_formula;
-
- assert(ctlFormula);
+ if(RT::args.tscc_flag){
+ TheFormula->unparse(myprinter, kc::internal);
+ StatePredicate *result = TheFormula->formula;
+
+ assert(result);
+ RT::rep->status("processed formula with %d atomic propositions",
+ result->countAtomic());
+ RT::data["analysis"]["formula"]["atomic_propositions"] =
static_cast<int>(result->countAtomic());
+
+ spFormula = result;
+ }else{
+
+ TheFormula->unparse(myprinter, kc::ctl);
+ ctlFormula = TheFormula->ctl_formula;
+
+ assert(ctlFormula);
+ }
break;
}
@@ -875,8 +892,13 @@
{
tsccExploration = new TSCCExplorationAGEF();
}
+ else
+ {
+ tsccExploration = new TSCCExplorationAGAF();
+ }
+ assert(spFormula);
p = new StatePredicateProperty(spFormula);
- fl = new FirelistStubbornAgef(p);
+ fl = new FirelistStubbornTscc(p);
}
break;
--
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.
