← Back to branch summary

~tapaal-ltl/verifypn/rule-D-fix

« back to all changes in this revision

Viewing changes to PetriEngine/Reachability/RandomQueryGenerator.cpp

  • Committer: Jonas Finnemann Jensen
  • Date: 2011-09-15 13:30:00 UTC
  • Revision ID: jopsen@gmail.com-20110915133000-wnywm1odf82emiuw
Import of sources from github

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Reachability/RandomQueryGenerator.cpp
 
1
/* PeTe - Petri Engine exTremE
 
2
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
 
3
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
 
4
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
 
5
 *
 
6
 * This program is free software: you can redistribute it and/or modify
 
7
 * it under the terms of the GNU General Public License as published by
 
8
 * the Free Software Foundation, either version 3 of the License, or
 
9
 * (at your option) any later version.
 
10
 *
 
11
 * This program is distributed in the hope that it will be useful,
 
12
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
13
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
14
 * GNU General Public License for more details.
 
15
 *
 
16
 * You should have received a copy of the GNU General Public License
 
17
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
18
 */
 
19
#include "RandomQueryGenerator.h"
 
20
 
 
21
#include "../PQL/PQL.h"
 
22
#include "../PQL/Contexts.h"
 
23
#include "../Structures/StateSet.h"
 
24
#include "../Structures/StateAllocator.h"
 
25
 
 
26
#include <sstream>
 
27
#include <list>
 
28
#include <string.h>
 
29
#include <stdlib.h>
 
30
#include <stdio.h>
 
31
#include <time.h>
 
32
 
 
33
using namespace std;
 
34
using namespace PetriEngine::PQL;
 
35
using namespace PetriEngine::Structures;
 
36
 
 
37
namespace PetriEngine {
 
38
namespace Reachability {
 
39
 
 
40
/** Generate a random query */
 
41
std::string RandomQueryGenerator::gen(const PetriNet& net,
 
42
                                                                          const MarkVal* m0,
 
43
                                                                          const VarVal* v0){
 
44
        srand(time(0)); // Chosen by fair dice roll
 
45
 
 
46
        StateAllocator<> allocator(net);
 
47
        State* s = allocator.createState();
 
48
        memcpy(s->marking(), m0, sizeof(MarkVal)*net.numberOfPlaces());
 
49
        memcpy(s->valuation(), v0, sizeof(VarVal)*net.numberOfVariables());
 
50
 
 
51
        int countdown = rand() % 5000000;
 
52
 
 
53
        State* ns = allocator.createState();
 
54
        while(countdown-- > 0){
 
55
                unsigned int  tstart = rand() % net.numberOfTransitions();
 
56
                bool done = false;
 
57
                for(unsigned int t = tstart; t < net.numberOfTransitions(); t++){
 
58
                        if(net.fire(t, s, ns)){
 
59
                                done = true;
 
60
                                tstart = 0;
 
61
                                break;
 
62
                        }
 
63
                }
 
64
                for(unsigned int t = 0; t < tstart; t++){
 
65
                        if(net.fire(t, s, ns)){
 
66
                                done = true;
 
67
                                break;
 
68
                        }
 
69
                }
 
70
                if(!done)
 
71
                        return "";
 
72
                else{
 
73
                        State* tmp = s;
 
74
                        s = ns;
 
75
                        ns = tmp;
 
76
                }
 
77
        }
 
78
        stringstream ss;
 
79
        ss<<net.placeNames()[0]<<" == "<<s->marking()[0];
 
80
        for(unsigned int p = 1; p < net.numberOfPlaces(); p++)
 
81
                ss<<" and "<<net.placeNames()[p]<<" == "<<s->marking()[p];
 
82
        for(unsigned int x = 0; x < net.numberOfVariables(); x++)
 
83
                ss<<" and "<<net.variableNames()[x]<<" == "<<s->valuation()[x];
 
84
        return ss.str();
 
85
}
 
86
 
 
87
} // Reachability
 
88
} // PetriEngine