idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

[ papers ] Implement proof-search for EF, AF, EG, AG

Browse Source 
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]
 )
This commit is contained in:
Thomas E. Hansen 2022-09-05 14:46:41 +02:00 committed by CodingCellist
parent f96b25a3d7
commit b3a8d344e4
1 changed files with 22 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
libs/papers/Search/CTL.idr
View File

@ -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)