fix ci

Author: hooopo

.github/workflows/ci.yml

@@ -40,4 +40,5 @@ jobs:
         sudo apt-get install graphviz
         gem install bundler
         bundle install --jobs 4 --retry 3
+        bundle exec rake app:wf
         bundle exec rails app:db:create && bundle exec rails app:db:migrate  && bundle exec rails test

app/models/wf/lola.rb

@@ -1,30 +1,5 @@
 # frozen_string_literal: true
 
-## generate lola format file.
-
-# PLACE P1,P2,P3;
-
-# MARKING P1;
-
-# TRANSITION T1
-# CONSUME P1:1;
-# PRODUCE P3:1;
-
-# TRANSITION T2
-# CONSUME P3:1;
-# PRODUCE P2:1;
-
-## checking
-
-# reachability of final marking
-# lola /Users/hooopo/w/wf/test/dummy/tmp/1-1582990693.lola --formula="AGEF(P1 = 0 AND P3 = 0 AND P2 = 1)" --json=/Users/hooopo/w/wf/test/dummy/tmp/1-reachability_of_final_marking.json
-
-# quasiliveness
-# lola /Users/hooopo/w/wf/test/dummy/tmp/1-1582990693.lola --formula="AG NOT FIREABLE (T1)" --json=/Users/hooopo/w/wf/test/dummy/tmp/1-dead_transition_1.json
-# lola /Users/hooopo/w/wf/test/dummy/tmp/1-1582990693.lola --formula="AG NOT FIREABLE (T2)" --json=/Users/hooopo/w/wf/test/dummy/tmp/1-dead_transition_2.json
-# deadlock
-# lola /Users/hooopo/w/wf/test/dummy/tmp/1-1582990693.lola --formula="EF (DEADLOCK AND (P2 = 0))" --json=/Users/hooopo/w/wf/test/dummy/tmp/1-deadlock.json
-
 module Wf
   class Lola
     attr_reader :end_p, :start_p, :workflow
@@ -77,13 +52,6 @@ def soundness?
       reachability_of_final_marking? && quasiliveness? && !deadlock?
     end
 
-    def deadlock?
-      formula = "EF (DEADLOCK AND (#{end_p.lola_id} = 0))"
-      result = run_cmd(formula, "deadlock")
-      result.dig("analysis", "result")
-    end
-
-    # reachability of final marking
     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"
@@ -96,6 +64,12 @@ def quasiliveness?
       workflow.transitions.all? { |t| !dead_transition?(t) }
     end
 
+    def deadlock?
+      formula = "EF (DEADLOCK AND (#{end_p.lola_id} = 0))"
+      result = run_cmd(formula, "deadlock")
+      result.dig("analysis", "result")
+    end
+
     private
 
       def dead_transition?(transition)

lib/tasks/wf_tasks.rake

@@ -10,6 +10,6 @@ task wf: :environment do
   puts `cd #{Rails.root.join("tmp")} && tar -zxvf lola.tar.gz`
   puts `cd #{Rails.root.join("tmp/lola-2.0")} && ./configure`
   puts `cd #{Rails.root.join("tmp/lola-2.0")} && make`
-  puts `cd #{Rails.root.join("tmp/lola-2.0")} && make install`
+  puts `cd #{Rails.root.join("tmp/lola-2.0")} && sudo make install`
   puts `lola --help`
 end

lib/wf.rb

@@ -39,5 +39,5 @@ class << self
   self.user_class                = "::Wf::User"
   self.org_classes               = { group: "::Wf::Group" }
   self.finish_conditions         = ["Wf::MultipleInstances::AllFinish"]
-  self.use_lola                  = true
+  self.use_lola                  = false
 end

lola.md

@@ -15,3 +15,33 @@ LoLA can answer reachability queries using the flag '-f' followed by 'REACHABLE'
 Positive reachability queries can be witnessed by a state and a path using flags -s and -p respectively.
 
 The tool documentation can be found at http://download.gna.org/service-tech/lola/lola.pdf.
+
+## Check Workflow Net
+
+```
+## generate lola format file.
+
+# PLACE P1,P2,P3;
+
+# MARKING P1;
+
+# TRANSITION T1
+# CONSUME P1:1;
+# PRODUCE P3:1;
+
+# TRANSITION T2
+# CONSUME P3:1;
+# PRODUCE P2:1;
+
+## checking
+
+# reachability of final marking
+# lola /Users/hooopo/w/wf/test/dummy/tmp/1-1582990693.lola --formula="AGEF(P1 = 0 AND P3 = 0 AND P2 = 1)" --json=/Users/hooopo/w/wf/test/dummy/tmp/1-reachability_of_final_marking.json
+
+# quasiliveness
+# lola /Users/hooopo/w/wf/test/dummy/tmp/1-1582990693.lola --formula="AG NOT FIREABLE (T1)" --json=/Users/hooopo/w/wf/test/dummy/tmp/1-dead_transition_1.json
+# lola /Users/hooopo/w/wf/test/dummy/tmp/1-1582990693.lola --formula="AG NOT FIREABLE (T2)" --json=/Users/hooopo/w/wf/test/dummy/tmp/1-dead_transition_2.json
+# deadlock
+# lola /Users/hooopo/w/wf/test/dummy/tmp/1-1582990693.lola --formula="EF (DEADLOCK AND (P2 = 0))" --json=/Users/hooopo/w/wf/test/dummy/tmp/1-deadlock.json
+```
+