From b3a8d344e4fff8b6c882ad1ff37b34b62ac18111 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Mon, 5 Sep 2022 14:46:41 +0200
Subject: [PATCH] [ papers ] Implement proof-search for EF, AF, EG, AG

This also caught an implementation error in the Global formula
definitions:
AG f = A[ f U (f AND' Completed) ]
and **not**
AG f = A[ (f U f) AND' Completed ]
(both of which are valid parsings of the original
 AG f = A[ f u f AND' Completed]
 )
---
 libs/papers/Search/CTL.idr | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/libs/papers/Search/CTL.idr b/libs/papers/Search/CTL.idr
index 2cca729cd..6bddab3a2 100644
--- a/libs/papers/Search/CTL.idr
+++ b/libs/papers/Search/CTL.idr
@@ -275,12 +275,12 @@ parameters (Lbls, Sts : Type)
   ||| We can only handle always global checks on finite paths.
   public export
   AlwaysGlobal : (f : Formula) -> Formula
-  AlwaysGlobal f = (AlwaysUntil f f) `AND'` Completed
+  AlwaysGlobal f = AlwaysUntil f (f `AND'` Completed)
 
   ||| We can only handle exists global checks on finite paths.
   public export
   ExistsGlobal : (f : Formula) -> Formula
-  ExistsGlobal f = (ExistsUntil f f) `AND'` Completed
+  ExistsGlobal f = ExistsUntil f (f `AND'` Completed)
 
   ------------------------------------------------------------------------
   -- Proof search (finally!)
@@ -341,3 +341,23 @@ parameters (Lbls, Sts : Type)
       rest : HDec (Lazy.Quantifiers.Any.Any (ExistsUntil f g n) ms)
       rest = HDecidable.LazyList.any ms (\ m => euSearch p1 p2 m n)
 
+  ||| Proof-search for Exists Finally
+  public export
+  efSearch : {f : _} -> MC f -> MC (ExistsFinally f)
+  efSearch g = euSearch (\ _, _ => yes TT) g
+
+  ||| Proof-search for Always Finally
+  public export
+  afSearch : {f : _} -> MC f -> MC (AlwaysFinally f)
+  afSearch g = auSearch (\ _, _ => yes TT) g
+
+  ||| Proof-search for Exists Global
+  public export
+  egSearch : {f : _} -> MC f -> MC (ExistsGlobal f)
+  egSearch g = euSearch g (g `mcAND'` isCompleted)
+
+  ||| Proof-search for Always Global
+  public export
+  agSearch : {f : _} -> MC f -> MC (AlwaysGlobal f)
+  agSearch g = auSearch g (g `mcAND'` isCompleted)
+