← Back to branch summary

~verifypn-maintainers/verifypn/u4.1

« back to all changes in this revision

Viewing changes to include/LTL/Simplification/SpotToPQL.h

  • Committer: Jiri Srba
  • Date: 2021-08-05 19:57:19 UTC
  • mfrom: (234.1.39 ltl-spring-2021)
  • Revision ID: srba@cs.aau.dk-20210805195719-tyf98wgglgn8xd0d
merged in lp:~tapaal-ltl/verifypn/ltl-spring-2021 adding many additions to LTL model checker (automata based methods for partial order and heuristic) and trace generation

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/LTL/Simplification/SpotToPQL.h
1
 
/* Copyright (C) 2020  Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
2
 
 *                     Simon M. Virenfeldt <simon@simwir.dk>
3
 
 *
4
 
 * This program is free software: you can redistribute it and/or modify
5
 
 * it under the terms of the GNU General Public License as published by
6
 
 * the Free Software Foundation, either version 3 of the License, or
7
 
 * (at your option) any later version.
8
 
 *
9
 
 * This program is distributed in the hope that it will be useful,
10
 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11
 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12
 
 * GNU General Public License for more details.
13
 
 *
14
 
 * You should have received a copy of the GNU General Public License
15
 
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
16
 
 */
17
 
 
18
 
#ifndef VERIFYPN_SPOTTOPQL_H
19
 
#define VERIFYPN_SPOTTOPQL_H
20
 
 
21
 
#include "PetriEngine/PQL/Expressions.h"
22
 
#include "LTL/LTLToBuchi.h"
23
 
#include <spot/tl/formula.hh>
24
 
 
25
 
namespace LTL {
26
 
    /**
27
 
     * Transform a Spot formula back into the PQL expression tree form.
28
 
     * @param formula The formula to translate to PQL
29
 
     * @param apinfo List of atomic propositions in the formula. This should have been created by {@link LTL::to_spot_formula}.
30
 
     * @return A PQL formula equivalent to the passed spot formula.
31
 
     */
32
 
    PetriEngine::PQL::Condition_ptr toPQL(const spot::formula &formula, const APInfo &apinfo);
33
 
 
34
 
    /**
35
 
     * Simplify an LTL formula using Spot's formula simplifier. Throws if formula is not valid LTL.
36
 
     * @param formula The formula to simplify.
37
 
     * @return the simplified formula.
38
 
     */
39
 
    PetriEngine::PQL::Condition_ptr simplify(const PetriEngine::PQL::Condition_ptr &formula, APCompression compress = APCompression::Choose);
40
 
}
41
 
 
42
 
#endif // VERIFYPN_SPOTTOPQL_H