Class: Wf::Lola

Inherits:
Object
  • Object
show all
Defined in:
app/models/wf/lola.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(workflow) ⇒ Lola

Returns a new instance of Lola.



6
7
8
9
10
11
 
# File 'app/models/wf/lola.rb', line 6

def initialize(workflow)
  @workflow = workflow
  @start_p  = workflow.places.start.first
  @end_p    = workflow.places.end.first
  generate_lola_file!
end

Instance Attribute Details

#end_p ⇒ Object (readonly)

Returns the value of attribute end_p.



5
6
7
 
# File 'app/models/wf/lola.rb', line 5

def end_p
  @end_p
end

#start_p ⇒ Object (readonly)

Returns the value of attribute start_p.



5
6
7
 
# File 'app/models/wf/lola.rb', line 5

def start_p
  @start_p
end

#workflow ⇒ Object (readonly)

Returns the value of attribute workflow.



5
6
7
 
# File 'app/models/wf/lola.rb', line 5

def workflow
  @workflow
end

Instance Method Details

#deadlock? ⇒ Boolean

Returns:

  • (Boolean) 


67
68
69
70
71
 
# File 'app/models/wf/lola.rb', line 67

def deadlock?
  formula = "EF (DEADLOCK AND (#{end_p.lola_id} = 0))"
  result = run_cmd(formula, "deadlock")
  result.dig("analysis", "result")
end

#generate_lola_file! ⇒ Object 



47
48
49
 
# File 'app/models/wf/lola.rb', line 47

def generate_lola_file!
  File.open(lola_path, "w") { |f| f.write(Wf::Lola.new(workflow).to_text) } unless File.exist?(lola_path)
end

#json_path(bucket) ⇒ Object 



39
40
41
 
# File 'app/models/wf/lola.rb', line 39

def json_path(bucket)
  Rails.root.join("tmp", "#{workflow.id}-#{bucket}.json")
end

#lola_path ⇒ Object 



43
44
45
 
# File 'app/models/wf/lola.rb', line 43

def lola_path
  Rails.root.join("tmp", "#{workflow.id}-#{workflow.updated_at.to_i}.lola")
end

#quasiliveness? ⇒ Boolean

Returns:

  • (Boolean) 


63
64
65
 
# File 'app/models/wf/lola.rb', line 63

def quasiliveness?
  workflow.transitions.all? { |t| !dead_transition?(t) }
end

#reachability_of_final_marking? ⇒ Boolean

Returns:

  • (Boolean) 


55
56
57
58
59
60
61
 
# File 'app/models/wf/lola.rb', line 55

def reachability_of_final_marking?
  formula = workflow.places.reject { |p| p == end_p }.map { |p| "#{p.lola_id} = 0" }.join(" AND ")
  formula += " AND #{end_p.lola_id} >= 1"
  formula = "AGEF(#{formula})"
  result = run_cmd(formula, "reachability_of_final_marking")
  result.dig("analysis", "result")
end

#soundness? ⇒ Boolean

Returns:

  • (Boolean) 


51
52
53
 
# File 'app/models/wf/lola.rb', line 51

def soundness?
  reachability_of_final_marking? && quasiliveness? && !deadlock?
end

#to_text ⇒ Object 



13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
 
# File 'app/models/wf/lola.rb', line 13

def to_text
  places      = workflow.places
  transitions = workflow.transitions

  places_text  = places.map(&:lola_id).join(",")
  marking_text = start_p.lola_id
  # TODO: with guard
  transitions_text = transitions.map do |t|
    consume = t.arcs.in.map { |arc| "#{arc.place.lola_id}:1" }.join(",")
    produce = t.arcs.out.map { |arc| "#{arc.place.lola_id}:1" }.join(",")
    [
      "TRANSITION #{t.lola_id}",
      "CONSUME #{consume};",
      "PRODUCE #{produce};"
    ].join("\n")
  end.join("\n\n")

  <<~LOLA
    PLACE #{places_text};

    MARKING #{marking_text};

    #{transitions_text}
  LOLA
end