← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to CTL/PetriNets/PetriConfig.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
CTL/PetriNets/PetriConfig.h
1
 
#ifndef PETRICONFIG_H
2
 
#define PETRICONFIG_H
3
 
 
4
 
#include <sstream>
5
 
#include "../DependencyGraph/Configuration.h"
6
 
#include "PetriEngine/PQL/PQL.h"
7
 
 
8
 
namespace PetriNets {
9
 
 
10
 
class PetriConfig : public DependencyGraph::Configuration {
11
 
 
12
 
public:
13
 
    using Condition = PetriEngine::PQL::Condition;
14
 
    PetriConfig() : 
15
 
        DependencyGraph::Configuration(), marking(0), query(NULL) 
16
 
    {}
17
 
    
18
 
    PetriConfig(size_t t_marking, Condition *t_query) :
19
 
        DependencyGraph::Configuration(), marking(t_marking), query(t_query) {
20
 
    }
21
 
 
22
 
    virtual ~PetriConfig(){};
23
 
 
24
 
    size_t marking;
25
 
    Condition *query;
26
 
 
27
 
};
28
 
 
29
 
}
30
 
#endif // PETRICONFIG_H