Class: PgVerify::Model::ParsedExpression

Inherits:
Object
  • Object
show all
Defined in:
lib/pg-verify/model/parsed_expression.rb

Constant Summary collapse

TYPE_GUARD =

Guards and preconditions

:guard
TYPE_ACTION =

Actions

:action
TYPE_TERM =

Term for the right part of an action

:term
TYPE_PL =

Propositional logic

:pl
TYPE_TL =

Temporal logic (LTL or CTL)

:tl
TYPE_LTL =

Linear temporal logic

:ltl
TYPE_CTL =

Computation tree logic

:ctl
TYPES = 
[ TYPE_GUARD, TYPE_ACTION, TYPE_TERM, TYPE_PL, TYPE_TL, TYPE_LTL, TYPE_CTL ]
LTL_KEYWORDS = 
"GFXRU".chars
CTL_KEYWORDS = 
[ "A", "E" ].product([ "G", "F", "X", "U" ]).map { |a, e| "#{a}#{e}" }

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(expression_string, type, source_location: nil) ⇒ ParsedExpression

Returns a new instance of ParsedExpression.



30
31
32
33
34
35
36
37
 
# File 'lib/pg-verify/model/parsed_expression.rb', line 30

def initialize(expression_string, type, source_location: nil)
    expression_string = expression_string.to_s if expression_string.is_a?(Symbol)
    raise "Unknown expression type '#{type}'" unless TYPES.include?(type)
    raise "Not a string '#{expression_string}'::#{expression_string.class}" unless expression_string.is_a?(String)
    @expression_string = expression_string
    @source_location = source_location
    @type = type
end

Instance Attribute Details

#expression_string ⇒ Object

Returns the value of attribute expression_string.



26
27
28
 
# File 'lib/pg-verify/model/parsed_expression.rb', line 26

def expression_string
  @expression_string
end

#source_location ⇒ Object

Returns the value of attribute source_location.



27
28
29
 
# File 'lib/pg-verify/model/parsed_expression.rb', line 27

def source_location
  @source_location
end

#type ⇒ Object

Returns the value of attribute type.



28
29
30
 
# File 'lib/pg-verify/model/parsed_expression.rb', line 28

def type
  @type
end

Instance Method Details

#assigned_variables ⇒ Object 



72
73
74
75
76
77
 
# File 'lib/pg-verify/model/parsed_expression.rb', line 72

def assigned_variables()
    raise "Not an action" unless @type == TYPE_ACTION
    return expression_string.split("|").map { |sub_action|
        sub_action.split(":=")[0].strip
    }
end

#predict_type ⇒ Object 



47
48
49
50
51
 
# File 'lib/pg-verify/model/parsed_expression.rb', line 47

def predict_type()
    return @type unless @type == :tl
    tokens = self.tokenize()
    return CTL_KEYWORDS.any? { |kw| tokens.include?(kw) } ? :ctl : :ltl
end

#to_s ⇒ Object 



68
69
70
 
# File 'lib/pg-verify/model/parsed_expression.rb', line 68

def to_s()
    @expression_string
end

#tokenize ⇒ Object

Splits the expression string into an array of tokens. e.g: “(a == b) && 3 >= 2” becomes [ “(”, “a”, “==”, “b”, “)”, “&&”, “3”, “>=”, “2” ] Note that this split method very much a hack at the moment



56
57
58
59
60
61
62
63
64
65
66
 
# File 'lib/pg-verify/model/parsed_expression.rb', line 56

def tokenize()
    return expression_string.split(/\s+/).map { |t|
        t.end_with?(")") ? [ t.chop, ")" ] : t
    }.flatten.map { |t|
        t.end_with?("(") ? [ t.chop, "(" ] : t
    }.flatten.map { |t|
        t.start_with?(")") ? [ ")" , t.slice(1..-1)] : t
    }.flatten.map { |t|
        t.start_with?("(") ? [ "(" , t.slice(1..-1)] : t
    }.flatten.reject(&:blank?)
end

#word_tokens ⇒ Object 



39
40
41
42
43
44
45
 
# File 'lib/pg-verify/model/parsed_expression.rb', line 39

def word_tokens()
    words = expression_string.scan(/[a-zA-Z_][a-zA-Z0-9_]*/).flatten.compact
    words = words.reject { |w| LTL_KEYWORDS.include?(w) }
    words = words.reject { |w| CTL_KEYWORDS.include?(w) }
    words = words.reject { |w| w == "TRUE" || w == "FALSE" }
    return words.map(&:to_sym)
end