Commit 22b6a492 authored by Benoît Barbot's avatar Benoît Barbot

small progress

parent 623c5b8f
Pipeline #989 failed with stages
in 3 minutes and 3 seconds
const double T=150;
const double T=200;
const double invT=0.005;
const double Ttrans=0;
VariablesList = {time,DISC countT, t_a, t_b, PLVAR_powerState, PLVAR_B12O1, PLVAR_B12O2, PLVAR_B12O3} ;
LocationsList = {l0, l1,l2};
Valid=PROB;
remain=AVG(Last(PLVAR_B12O2));
Throughput_t_a= AVG(Last(t_a));
Throughput_t_b= AVG(Last(t_b));
MeanToken_powerState= AVG(Last( PLVAR_powerState));
......@@ -22,4 +23,4 @@ Edges={
((l1,l1),{t_b},time<=T,{t_b = t_b + invT, countT = countT+1 });
((l1,l1),{time_0_0,time_1_0,time_2_0,SynchIN15,Synch12O1,Synch12O2,Synch12O3,Synctrans},time<=T, # );
((l1,l2),#,time=T ,#);
};
\ No newline at end of file
};
pta
module originator
o : [0..1] init 0;
x : clock;
y : clock;
invariant
(o=0) => (x<=1)&(y<=1)
(x<=1)&(y<=1)
endinvariant
[a] (o=0) & (x<1)&(x>0) -> (o'=1) & (y'=0);
[b] (o=1) & (y<1)& (x<1)&(x>0)&(y>0) -> (o'=0) & (x'=0) & (y'=0);
[a] (o=0) & (x<1) -> (o'=1) & (y'=0);
[a] (o=1) & (y<1)&(x<1) -> (o'=0) & (x'=0) & (y'=0);
endmodule
......@@ -35,13 +35,13 @@ using namespace std;
template<class DEDState>
void LHA_orig<DEDState>::copyState(LHA_orig *A){
this->Vars = A->Vars;
this->LinForm.swap(A->LinForm);
this->OldLinForm.swap(A->OldLinForm);
this->LhaFunc.swap(A->LhaFunc);
this->Likelihood = A->Likelihood;
this->CurrentTime =A->CurrentTime;
this->CurrentLocation=A->CurrentLocation;
this->Vars = A->Vars;
this->LinForm.swap(A->LinForm);
this->OldLinForm.swap(A->OldLinForm);
this->LhaFunc.swap(A->LhaFunc);
this->Likelihood = A->Likelihood;
this->CurrentTime =A->CurrentTime;
this->CurrentLocation=A->CurrentLocation;
}
......@@ -60,7 +60,7 @@ void LHA_orig<DEDState>::fireAutonomous(int EdgeIndex,const DEDState &M){
/**
* Find a suitable syncronized transitions in the LHA
* Find a suitable syncronized transitions in the LHA
* @param tr a SPN transiiton index
* @param M is the marking of the SPN
* @param b a binding of the colored variable of the SPN for the transition.
......@@ -68,7 +68,7 @@ void LHA_orig<DEDState>::fireAutonomous(int EdgeIndex,const DEDState &M){
template<class DEDState>
int LHA_orig<DEDState>::synchroniseWith(size_t tr, const DEDState& m,const abstractBinding& b){
//Check if there exist a valid transition in the automata.
int SE = GetEnabled_S_Edges(tr, m, b);
if (SE >= 0) {
......@@ -97,11 +97,11 @@ AutEdge LHA_orig<DEDState>::GetEnabled_A_Edges(const DEDState& Marking) {
Ed.Index = it;
Ed.FiringTime = I.first;
}
}
}
}
return Ed;
}
......@@ -113,10 +113,10 @@ AutEdge LHA_orig<DEDState>::GetEnabled_A_Edges(const DEDState& Marking) {
template<class DEDState>
void LHA_orig<DEDState>::updateLHA(double DeltaT, const DEDState &Marking){
this->DoElapsedTimeUpdate(DeltaT, Marking);
this->UpdateLinForm(Marking);
this->UpdateLhaFunc(DeltaT);
this->CurrentTime += DeltaT;
this->DoElapsedTimeUpdate(DeltaT, Marking);
this->UpdateLinForm(Marking);
this->UpdateLhaFunc(DeltaT);
this->CurrentTime += DeltaT;
}
......@@ -141,9 +141,9 @@ void LHA_orig<DEDState>::reset(const DEDState& Marking) {
*/
template<class DEDState>
void LHA_orig<DEDState>::getFinalValues(const DEDState& m,vector<double>& v,vector<bool>& v2){
this->UpdateLinForm(m);
this->UpdateFormulaVal(m);
v=this->FormulaVal;
this->UpdateLinForm(m);
this->UpdateFormulaVal(m);
v=this->FormulaVal;
v2=this->FormulaValQual;
}
......@@ -258,4 +258,3 @@ double LHA<DEDState>::BoxedIntegral(double OldInt, double t, double Delta, doubl
//#include "MarkovChain.hpp"
//template class LHA<State>;
//template class LHA_orig<State>;
......@@ -55,7 +55,7 @@ ostream& operator<<(ostream& f, const Poly<N>& p){
}else{
f<< "x_" << (j+1) << "^";
}
f << p[i].d[j]<< " ";
}
}
......@@ -81,7 +81,7 @@ std::vector<Poly<N>> parse(const std::string file){
vector<Poly<N>> polyT;
std::ifstream polyf(file);
if(polyf.is_open()){
std::cerr << "start reading:" << file << endl;
//std::cerr << "start reading:" << file << endl;
while( polyf.good()){
string line;
std::getline(polyf, line);
......@@ -106,7 +106,7 @@ std::vector<Poly<N>> parse(const std::string file){
polyT.push_back(p);
}
}
cerr << "Finish parsing found "<< polyT.size() <<" polynomes" << endl;
//cerr << "Finish parsing found "<< polyT.size() <<" polynomes" << endl;
return polyT;
}
......
......@@ -53,4 +53,3 @@ template class LHA_orig<abstractState>;*/
#include "SKModelBase.cpp"
template class SKModel<EventsQueue>;
template class SKModel<EventsQueueSet>;
......@@ -175,7 +175,8 @@ void KroneckerState::seed(unsigned long seed){
double KroneckerState::sample(){
double alpha = pow(phi_d,baseId);
//(5437*baseId + 3671) % 9973; // A simple random (I choose the parameters randomly) linear congruantial pseudo random number generator.
//double alpha = sqrt(boost::math::prime(baseId-1));
double d;
double sample = modf( seed_val + (double)it * alpha, &d);
if(P.verbose > 4)cerr << "Sampling Kronecker; seed: "<< seed_val << " base: "<< baseId << "\tn: "<< it << "\tbasealpha: " << phi_d << "\talpha: "<< alpha << "->" << sample << endl;
......@@ -197,8 +198,8 @@ void KroneckerState::newTrajectory(){
}
double timeGen::sampleQuasiRandom(size_t){
//return vanDerCorputSampler.sample();
return kroneckerSampler.sample();
return vanDerCorputSampler.sample();
//return kroneckerSampler.sample();
}
void timeGen::reset(){
......@@ -408,10 +409,10 @@ double timeGen::GenerateTime(DistributionType distribution,size_t trid, const ar
/*
//Isotrop Hack
//std::uniform_real_distribution<> unif(lower, upper);
//gentime = unif(RandomNumber);
gentime = sampleQuasiRandom(trid);
gentime = (upper-lower)*gentime + lower;
std::uniform_real_distribution<> unif(lower, upper);
gentime = unif(RandomNumber);
//gentime = sampleQuasiRandom(trid);
//gentime = (upper-lower)*gentime + lower;
cerr << cd.userDefineCDF(param,gentime) << endl;
return gentime;
//Isotrop Hack
......
This diff is collapsed.
......@@ -175,7 +175,7 @@ patient_Domain operator + (const patient_Token& t1 ,const patient_Token& t2 )
#define ABSTRACT_BINDING_h
class abstractBindingImpl {
public:
patient_Token x;
patient_Token x = patient_Token((patient_Color_Classe) 0);
};
#endif
class abstractMarkingImpl {
......
......@@ -312,7 +312,8 @@ abstractBinding& abstractBinding::operator = (const abstractBinding& m) {
return *this;
}
void abstractBinding::print()const{
std::cerr << "\tx: ";P->x.print(std::cerr);
std::cerr << "\tx: ";
P->x.print(std::cerr);
}
size_t abstractBinding::id()const{
return idcount;
......@@ -384,7 +385,7 @@ const int* SPN::FreeMarkDepT[] = {EMPTY_array, EMPTY_array, EMPTY_array, EMPTY_a
static spn_trans TransArray[21] = { _trans(0,DETERMINISTIC,0,20, 0), _trans(1,EXPONENTIAL,0,20, 0), _trans(2,EXPONENTIAL,0,20, 0), _trans(3,EXPONENTIAL,0,20, 0), _trans(4,EXPONENTIAL,0,20, 0), _trans(5,DETERMINISTIC,0,20, 0), _trans(6,DETERMINISTIC,0,20, 0), _trans(7,EXPONENTIAL,0,20, 0), _trans(8,DETERMINISTIC,0,20, 0), _trans(9,DETERMINISTIC,0,20, 0), _trans(10,DETERMINISTIC,0,20, 0), _trans(11,DETERMINISTIC,0,20, 0), _trans(12,EXPONENTIAL,0,20, 0), _trans(13,EXPONENTIAL,0,20, 0), _trans(14,EXPONENTIAL,0,20, 0), _trans(15,EXPONENTIAL,0,20, 0), _trans(16,DETERMINISTIC,0,20, 0), _trans(17,DETERMINISTIC,0,20, 0), _trans(18,EXPONENTIAL,0,20, 0), _trans(19,EXPONENTIAL,0,20, 0), _trans(20,EXPONENTIAL,0,20, 0), };
SPN::SPN():
customDistr(*(new CustomDistr())),pl(26), tr(21) ,Transition(TransArray,TransArray +21),Place(26),ParamDistr(),TransitionConditions(21,0){
Path ="Hospital.grml";
Path ="../../test/../Examples/Hospital/Hospital.grml";
{ //EXRayBlood
abstractBinding bl = Transition[0].bindingList[0];
Transition[0].bindingList[0] = bl;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment