← Back to branch summary

~srba/verifypn/u2.0

« back to all changes in this revision

Viewing changes to CTLParser/CTLOptimizer.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/CTLOptimizer.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:   CTLOptimizer.cpp
 
9
 * Author: mossns
 
10
 * 
 
11
 * Created on April 28, 2016, 1:54 PM
 
12
 */
 
13
 
 
14
#include "CTLOptimizer.h"
 
15
 
 
16
CTLOptimizer::CTLOptimizer() {
 
17
}
 
18
 
 
19
CTLOptimizer::CTLOptimizer(const CTLOptimizer& orig) {
 
20
}
 
21
 
 
22
CTLOptimizer::~CTLOptimizer() {
 
23
}
 
24
 
 
25
CTLQuery* CTLOptimizer::Optimize(CTLQuery *query) {
 
26
    query = OptimizeNegation(query);
 
27
    return query;
 
28
}
 
29
 
 
30
CTLQuery* CTLOptimizer::OptimizeNegation(CTLQuery *query) {
 
31
    CTLType query_type = query->GetQueryType();
 
32
    if(query_type == EVAL){
 
33
        return query;
 
34
    }
 
35
    else if (query_type == LOPERATOR){
 
36
        if(query->GetQuantifier() != NEG){
 
37
            query->SetFirstChild(OptimizeNegation(query->GetFirstChild()));
 
38
            query->SetSecondChild(OptimizeNegation(query->GetSecondChild()));
 
39
        }
 
40
        else {//Negation
 
41
            if(query->GetFirstChild()->GetQueryType() == LOPERATOR && query->GetFirstChild()->GetQuantifier() == NEG){
 
42
                query = query->GetFirstChild()->GetFirstChild();
 
43
                if(query->GetQueryType() == EVAL){
 
44
                    return query;
 
45
                }
 
46
                else if(query->GetQueryType() == LOPERATOR){
 
47
                    if(query->GetQuantifier() != NEG){
 
48
                        query->SetFirstChild(OptimizeNegation(query->GetFirstChild()));
 
49
                        query->SetSecondChild(OptimizeNegation(query->GetSecondChild()));
 
50
                    }
 
51
                    else{
 
52
                        query->SetFirstChild(OptimizeNegation(query->GetFirstChild()));
 
53
                    }
 
54
                }
 
55
                else if (query->GetQueryType() == PATHQEURY){
 
56
                    if (query->GetPath() == U){
 
57
                        query->SetFirstChild(OptimizeNegation(query->GetFirstChild()));
 
58
                        query->SetSecondChild(OptimizeNegation(query->GetSecondChild()));
 
59
                    }
 
60
                    else{
 
61
                        query->SetFirstChild(OptimizeNegation(query->GetFirstChild()));
 
62
                    }
 
63
                }
 
64
            }
 
65
        }
 
66
    }
 
67
    else if (query_type == PATHQEURY){
 
68
        if (query->GetPath() == U){
 
69
            query->SetFirstChild(OptimizeNegation(query->GetFirstChild()));
 
70
            query->SetSecondChild(OptimizeNegation(query->GetSecondChild()));
 
71
        }
 
72
        else{
 
73
            query->SetFirstChild(OptimizeNegation(query->GetFirstChild()));
 
74
        }
 
75
    }
 
76
    return query;
 
77
}