feat(ltl): First stab at an LTL checker

default.nix

@@ -7,6 +7,7 @@
 , nix-build-debugger  ? false
 , nix-build-generator ? true
 , nix-build-ldfi      ? false
+, nix-build-ltl       ? true
 , nix-build-scheduler ? false
 }:
 with pkgs;
@@ -20,6 +21,7 @@ let
   debugger = callPackage ./src/debugger/default.nix {};
   generator = callPackage ./src/generator/default.nix {};
   ldfi = callPackage ./src/ldfi2/default.nix {};
+  ltl = callPackage ./src/ltl/default.nix {};
   scheduler = callPackage ./src/scheduler/default.nix {};
 in
 
@@ -38,6 +40,7 @@ stdenv.mkDerivation {
                           ++ lib.optional (nix-build-all || nix-build-debugger)  [ debugger ]
                           ++ lib.optional (nix-build-all || nix-build-generator) [ generator ]
                           ++ lib.optional (nix-build-all || nix-build-ldfi)      [ ldfi ]
+                          ++ lib.optional (nix-build-all || nix-build-ltl)       [ ltl ]
                           ++ lib.optional (nix-build-all || nix-build-scheduler) [ scheduler ];
 
   installPhase = ''
@@ -83,6 +86,12 @@ stdenv.mkDerivation {
     install -D $src/ldfi2/ldfi2 $out/bin/detsys-ldfi
     ''
     }
+    ${if nix-build-ltl || nix-build-all then ''
+    install -D ${ltl.out}/bin/detsys-ltl $out/bin
+    '' else ''
+    install -D $src/ltl/ltl $out/bin/detsys-ltl
+    ''
+    }
     ${if nix-build-scheduler || nix-build-all then ''
     install -D ${scheduler.out}/bin/detsys-scheduler $out/bin
     '' else ''

src/lib/ltl.go

@@ -0,0 +1,31 @@
+package lib
+
+import (
+	"encoding/json"
+	"log"
+	"os"
+	"os/exec"
+	"strconv"
+	"time"
+)
+
+func LtlChecker(testId TestId, runId RunId, formula string) bool {
+	start := time.Now()
+	cmd := exec.Command("detsys-ltl", "check", "--testId", strconv.Itoa(testId.TestId), "--runId", strconv.Itoa(runId.RunId), "--formula", formula)
+	cmd.Stderr = os.Stderr
+
+	out, err := cmd.Output()
+
+	if err != nil {
+		panic(err)
+	}
+
+	var result struct {
+		Result bool `json:"result"`
+	}
+	err = json.Unmarshal(out, &result)
+	elapsed := time.Since(start)
+	log.Printf("LTL Checker time: %v\n", elapsed)
+
+	return result.Result
+}

src/ltl/CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for 
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

src/ltl/LICENSE

@@ -0,0 +1,3 @@
+Copyright (c) 2021 Symbiont Inc.
+
+All rights reserved.

src/ltl/app/Main.hs

@@ -0,0 +1,48 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import qualified Data.Aeson as Aeson
+import qualified Data.Aeson.Text as AesonText
+import qualified Data.Text.Lazy.IO as TextIO
+import Options.Generic
+
+import Ltl
+import Ltl.Json
+import qualified Ltl.Storage as Storage
+import Ltl.Prop.Parser (parse)
+
+data Config
+  = Check
+    { testId :: Int <?> "Which TestId to test",
+      runId :: Int <?> "Which RunId to test",
+      formula :: Text <?> "LTL Formula to check"
+    }
+  | Version
+  deriving (Generic)
+
+instance ParseRecord Config
+
+main :: IO ()
+main = do
+  (cfg, help) <- getWithHelp "LTL checker"
+  case cfg of
+    Version -> putStrLn "<GIT VERSION NOT IMPLEMENTED>"
+    Check{..} -> do
+      trace <- Storage.sqliteLoad (unHelpful testId) (unHelpful runId)
+      testFormula <- case parse (unHelpful formula) of
+        Left s -> error s
+        Right x -> pure x
+      let r = Result $ check testFormula trace
+      TextIO.putStrLn $ AesonText.encodeToLazyText r
+
+
+data Result = Result
+  { result :: Bool
+  } deriving (Generic)
+
+instance Aeson.FromJSON Result
+instance Aeson.ToJSON Result

src/ltl/cabal.project

@@ -0,0 +1,13 @@
+packages: .
+
+with-compiler: ghc-8.10.3
+
+reject-unconstrained-dependencies: all
+
+constraints: QuickCheck +old-random
+
+package ldfi
+  ghc-options: -Wall
+
+allow-older: *
+allow-newer: *