← Back to branch summary

~tapaal-dist-ctl/verifypn/escapeKey_issue_fix

« back to all changes in this revision

Viewing changes to CTL/CertainZeroFPA.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:
CTL/CertainZeroFPA.cpp
2
2
 
3
3
namespace ctl{
4
4
 
5
 
bool preprocessQuery(CTLTree *f) {
6
 
    
7
 
    bool isTemporal = f->quantifier == A || f->quantifier == E;
8
 
    if (f->quantifier == AND ||
9
 
            f->quantifier == OR ||
10
 
            (f->quantifier == A && f->path == U) ||
11
 
            (f->quantifier == E && f->path == U)) {
12
 
        //operand order guarantees subquery will be preprocessed
13
 
        isTemporal = preprocessQuery(f->second) || isTemporal;
14
 
        isTemporal = preprocessQuery(f->first) || isTemporal;
15
 
    }
16
 
    if (f->quantifier == NEG ||
17
 
            (f->path == G && (f->quantifier == A || f->quantifier == E)) ||
18
 
            (f->path == X && (f->quantifier == A || f->quantifier == E)) ||
19
 
            (f->path == F && (f->quantifier == A || f->quantifier == E))) {
20
 
        isTemporal = preprocessQuery(f->first) || isTemporal;
21
 
    }
22
 
    f->isTemporal = isTemporal;
23
 
    return isTemporal;
24
 
}
25
 
 
26
5
bool CertainZeroFPA::search(DependencyGraph &t_graph, AbstractSearchStrategy &W)
27
6
{
28
7
    PriorityQueue N;
29
8
 
30
9
    Configuration &v = t_graph.initialConfiguration();
31
10
    v.assignment = ZERO;
32
 
    preprocessQuery(v.query);
33
11
 
34
12
    for(Edge *e : t_graph.successors(v)){
35
13
        W.push(e);
48
26
            N.pop();
49
27
        }
50
28
 
 
29
//        e->edgePrinter();
 
30
 
51
31
        /*****************************************************************/
52
32
        /*Data handling*/
53
33
        int targetONEassignments = 0;
156
136
        e->processed = true;
157
137
    }
158
138
 
159
 
    //std::cout << "Final Assignment: " << v.assignment << " " << ((v.assignment == ONE) ? true : false) << std::endl;
 
139
//    std::cout << "Final Assignment: " << v.assignment << " " << ((v.assignment == ONE) ? true : false) << std::endl;
160
140
    return (v.assignment == ONE) ? true : false;
161
141
}
162
142