← Back to branch summary

~srba/verifypn/u2.0

« back to all changes in this revision

Viewing changes to CTLParser/EvaluateableProposition.cpp

merge in branch ParserRefactoring_The_Correct_One (new parser for CTL queries

Show diffs side-by-side

added added

removed removed

Lines of Context:
CTLParser/EvaluateableProposition.cpp
 
1
/*
 
2
 * To change this license header, choose License Headers in Project Properties.
 
3
 * To change this template file, choose Tools | Templates
 
4
 * and open the template in the editor.
 
5
 */
 
6
 
 
7
/* 
 
8
 * File:   EvaluateableProposition.cpp
 
9
 * Author: mossns
 
10
 * 
 
11
 * Created on April 27, 2016, 2:36 PM
 
12
 */
 
13
 
 
14
#include <string>
 
15
#include <stdexcept> 
 
16
#include <sstream>
 
17
 
 
18
#include "EvaluateableProposition.h"
 
19
#include "CTLParser.h"
 
20
 
 
21
namespace patch
 
22
{
 
23
    //A replacement for the standard to string function, which we cannot use because old OS X does not have c++11
 
24
    template < typename T > std::string to_string( const T& n )
 
25
    {
 
26
        std::ostringstream stm ;
 
27
        stm << n ;
 
28
        return stm.str() ;
 
29
    }
 
30
}
 
31
 
 
32
EvaluateableProposition::EvaluateableProposition(std::string a, PetriEngine::PetriNet *net) {
 
33
    if(a.substr(0,2).compare("in") == 0 || a.substr(0,2).compare("to") == 0){
 
34
        _type = CARDINALITY;
 
35
        _loperator = SetLoperator(a);
 
36
        assert(_loperator != NOT_CARDINALITY);
 
37
 
 
38
        size_t begin = a.find('(') + 1;
 
39
        size_t end = a.find(')') - begin;
 
40
        std::string first_parameter_str = a.substr(begin, end);
 
41
        a = a.substr(a.find(')') + 1);
 
42
 
 
43
        begin = a.find('(') + 1;
 
44
        end = a.find(')') - begin;
 
45
        std::string second_parameter_str = a.substr(begin, end);
 
46
        _firstParameter = CreateParameter(first_parameter_str, net->placeNames(), net->numberOfPlaces());
 
47
        _secondParameter = CreateParameter(second_parameter_str, net->placeNames(), net->numberOfPlaces());
 
48
    }
 
49
    else if(a.substr(0,2).compare("is") == 0){
 
50
        _type = FIREABILITY;
 
51
        _loperator = NOT_CARDINALITY;
 
52
        size_t s_pos = a.find('(') + 1;
 
53
        size_t e_pos = a.find(')') - 1;
 
54
        assert(s_pos < e_pos);
 
55
        int fire_str_length = e_pos - s_pos + 1;
 
56
        std::string fireset_str = a.substr(s_pos, fire_str_length);
 
57
        SetFireset(fireset_str, net->transitionNames(), net->numberOfTransitions());
 
58
    }
 
59
    else if(a.substr(0,2).compare("tr") == 0){
 
60
        
 
61
    }
 
62
    else if(a.substr(0,2).compare("fa") == 0){
 
63
        
 
64
    }
 
65
    else{
 
66
        assert(false && "Atomic string proposed for proposition could not be parsed");
 
67
    }
 
68
}
 
69
 
 
70
EvaluateableProposition::~EvaluateableProposition() {
 
71
}
 
72
 
 
73
PropositionType EvaluateableProposition::GetPropositionType(){
 
74
    return _type;
 
75
}
 
76
 
 
77
LoperatorType EvaluateableProposition::GetLoperator(){
 
78
    assert(_type == CARDINALITY && "Proposition is not a cardinality proposition");
 
79
    return _loperator;
 
80
}
 
81
 
 
82
std::vector<int> EvaluateableProposition::GetFireset() {
 
83
    assert(_type == FIREABILITY && "Proposition is not a fireability proposition");
 
84
    return _fireset;
 
85
}
 
86
 
 
87
void EvaluateableProposition::SetFireset(std::string fireset_str, std::vector<std::string> t_names, unsigned int numberof_t){
 
88
    std::string restof_firestring = fireset_str;
 
89
    while(restof_firestring.length() > 0){
 
90
        size_t position = restof_firestring.find(',');
 
91
        std::string current_t = restof_firestring.substr(0, position);
 
92
        for(int i = 0; i < numberof_t; i++){
 
93
            if (current_t.compare(t_names[i]) == 0){
 
94
                _fireset.push_back(i);
 
95
            }
 
96
        }
 
97
        if (position != -1)
 
98
            restof_firestring = restof_firestring.substr(position);
 
99
        else
 
100
            restof_firestring = "";
 
101
    }
 
102
    for ( auto f : _fireset){
 
103
        std::cout<<f<<" is id of "<< t_names[f]<<std::endl;
 
104
    }
 
105
}
 
106
 
 
107
CardinalityParameter* EvaluateableProposition::CreateParameter(std::string parameter_str, std::vector<std::string> p_names, unsigned int numberof_p){
 
108
    CardinalityParameter *param = new CardinalityParameter();
 
109
    std::string::size_type sz;    
 
110
    char c;
 
111
    if(sscanf(parameter_str.c_str(), "%d%c", &param->value, &c) == 1) {
 
112
        //If string is identifier starting with a number, you will read two items.
 
113
        //If it's an identifier starting with a character, you will read zero items.
 
114
        //The only time when you read just one item if the whole string is just numbers.
 
115
        param->isPlace = false;
 
116
    } else {    //error
 
117
        
 
118
        param->isPlace = true;
 
119
        std::vector<std::string> places_str;
 
120
        std::size_t found = parameter_str.find(",");
 
121
        
 
122
        while(found != parameter_str.npos){
 
123
            std::string temp = parameter_str.substr(0, found);
 
124
            places_str.push_back(temp);
 
125
            parameter_str = parameter_str.substr(found + 2);
 
126
            found = parameter_str.find(",");
 
127
        }
 
128
        
 
129
        places_str.push_back(parameter_str);
 
130
        
 
131
        for(int i = 0; i < numberof_p; i++){
 
132
            for(std::string place : places_str){
 
133
                if(p_names[i].compare(place) == 0){
 
134
                    param->places_i.push_back(i);
 
135
                }
 
136
            }
 
137
        }
 
138
    }
 
139
    return param;
 
140
}
 
141
 
 
142
LoperatorType EvaluateableProposition::SetLoperator(std::string atom_str){
 
143
    std::string loperator_str = atom_str.substr(atom_str.find(')'));
 
144
    loperator_str = loperator_str.substr(0, loperator_str.find('('));
 
145
    if(loperator_str.compare(" le "))
 
146
            return LEQ;
 
147
    else if (loperator_str.compare(" ge "))
 
148
        return GRQ;
 
149
    else if (loperator_str.compare(" eq "))
 
150
        return EQ;
 
151
    else assert(false && "Could not parse the given logical operator");
 
152
}
 
153
 
 
154
std::string EvaluateableProposition::ToString() {
 
155
    if (_type == FIREABILITY) {
 
156
        std::string fire_str = "Fireset(";
 
157
        for(auto f : _fireset){
 
158
            fire_str = fire_str + " " + patch::to_string(f);
 
159
        }
 
160
        return fire_str + ")";
 
161
    }
 
162
    else if (_type == CARDINALITY){
 
163
        std::string cardi_str = "(";
 
164
        if(_firstParameter->isPlace)
 
165
            cardi_str = cardi_str + "place(" + patch::to_string(_firstParameter->value) + ")";
 
166
        else
 
167
            cardi_str = cardi_str = patch::to_string(_firstParameter->value);
 
168
        
 
169
        cardi_str = cardi_str + " le ";
 
170
        
 
171
        if(_secondParameter->isPlace)
 
172
            cardi_str = cardi_str + "place(" + patch::to_string(_secondParameter->value) + ")";
 
173
        else
 
174
            cardi_str = cardi_str = patch::to_string(_secondParameter->value);
 
175
        return cardi_str + ")";
 
176
    }
 
177
    else
 
178
        assert(false && "Proposition had no type");
 
179
}
 
180
 
 
181
CardinalityParameter* EvaluateableProposition::GetFirstParameter() {
 
182
    assert(_type == CARDINALITY);
 
183
    return _firstParameter;
 
184
}
 
185
 
 
186
CardinalityParameter* EvaluateableProposition::GetSecondParameter() {
 
187
    assert(_type == CARDINALITY);
 
188
    return _secondParameter;
 
189
}