LTS (empty) → 0.1.0.0

raw patch · 9 files changed

+337/−0 lines, 9 filesdep +LTSdep +QuickCheckdep +basesetup-changed

Dependencies added: LTS, QuickCheck, base, criterion, fin, smallcheck, tasty, tasty-hunit, tasty-smallcheck, time

Files

CHANGELOG.md +5/−0
LICENSE +21/−0
LTS.cabal +66/−0
README.md +24/−0
Setup.hs +2/−0
bench/Main.hs +17/−0
programs/Main.hs +13/−0
src/Data/LTS.hs +144/−0
tests/Main.hs +45/−0

+ CHANGELOG.md view

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

+ LICENSE view

@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2020 Ajay Kumar Eeralla++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.

+ LTS.cabal view

@@ -0,0 +1,66 @@+name:                LTS+version:             0.1.0.0+synopsis:            LTS: Labelled Transition System+description:         This is an implementation of labelled transition system and+                     follow the README for information on importing and getting started.+license:             MIT+license-file:        LICENSE+author:              Ajay Kumar Eeralla+maintainer:          aeeralla@galois.com+copyright:           ©2020 Ajay Kumar Eeralla+category:            State Machines+build-type:          Simple+cabal-version:       >=1.10+tested-with:         GHC == 8.2.2+                     GHC == 8.4.4+                     GHC == 8.6.5+                     GHC == 7.10.3+++extra-source-files:  CHANGELOG.md, README.md++Source-Repository head+  type:     git+  location: git@github.com:ajayeeralla/LTS.git++library+  default-language: Haskell2010+  hs-source-dirs:   src+  exposed-modules:+    Data.LTS++  build-depends:      base >= 4.8.2.0 && <5+                    , fin >= 0.1.1 && < 0.2+executable LTS+  default-language:    Haskell2010+  build-depends:      LTS+                    , base                  +  hs-source-dirs:     programs+  main-is:            Main.hs+  ghc-options:        -O2 -fno-warn-unused-do-bind++test-suite lts-tests+  default-language:   Haskell2010+  type:               exitcode-stdio-1.0+  hs-source-dirs:     tests+  main-is:            Main.hs+  build-depends:      LTS+                    , QuickCheck ==2.14+                    , base+                    , tasty+                    , tasty-smallcheck+                    , tasty-hunit+                    , smallcheck+  ghc-options:        -O2 -fno-warn-unused-do-bind++benchmark lts-bench+  default-language:   Haskell2010+  type:               exitcode-stdio-1.0+  hs-source-dirs:     bench+  main-is:            Main.hs+  build-depends:      LTS+                    , base+                    , time+                    , criterion++  ghc-options:        -O2

+ README.md view

@@ -0,0 +1,24 @@+## LTS: Labelled Transition System+[![Travis](https://api.travis-ci.com/ajayeeralla/LTS.svg?branch=master)](https://travis-ci.com/github/ajayeeralla/LTS)+[![MIT license](https://img.shields.io/badge/license-MIT-blue.svg)](https://github.com/ajayeeralla/LTS/edit/master/LICENSE)++This is a library that implements a [labelled transition system](https://en.wikipedia.org/wiki/Transition_system) that can be either deterministic or non-deterministic.++## Example++Here is an example to use LTS library:++```+import Data.LTS++main = do+    let s0 :: LTSState Int = LTSState {stateId=0, out=3}+    let s1 :: LTSState Int = LTSState {stateId=1, out=5}+    let s2 :: LTSState Int = LTSState {stateId=2, out=7}+    let t1 :: Transition Int Char = Transition {transitionFrom=s0, transitionGuard='a', transitionTo=s1}+    let t2 :: Transition Int Char = Transition {transitionFrom=s1, transitionGuard='b', transitionTo=s2}++    putStrLn "depth of LTS [t1, t2]:"+    print (depth [t1, t2] s0)+```+

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ bench/Main.hs view

@@ -0,0 +1,17 @@+{-# LANGUAGE ScopedTypeVariables #-}++module Main where+import Criterion.Main+import Data.LTS++s0 :: LTSState Int = LTSState {stateId=0, out=3}+s1 :: LTSState Int = LTSState {stateId=1, out=5}+s2 :: LTSState Int = LTSState {stateId=2, out=7}+t1 :: Transition Int Char = Transition {transitionFrom=s0, transitionGuard='a', transitionTo=s1}+t2 :: Transition Int Char = Transition {transitionFrom=s1, transitionGuard='b', transitionTo=s2}++main = defaultMain [+  bgroup "Depth" [ bench "1"  $ whnf depth [t1]+                 , bench "5"  $ whnf depth [t1, t2]+                 ]+  ]

+ programs/Main.hs view

@@ -0,0 +1,13 @@+{-# LANGUAGE ScopedTypeVariables #-}++import Data.LTS++main = do+    let s0 :: LTSState Int = LTSState {stateId=0, out=3}+    let s1 :: LTSState Int = LTSState {stateId=1, out=5}+    let s2 :: LTSState Int = LTSState {stateId=2, out=7}+    let t1 :: Transition Int Char = Transition {transitionFrom=s0, transitionGuard='a', transitionTo=s1}+    let t2 :: Transition Int Char = Transition {transitionFrom=s1, transitionGuard='b', transitionTo=s2}++    putStrLn "depth of LTS [t1, t2]:"+    print (depth [t1, t2] s0)

+ src/Data/LTS.hs view

@@ -0,0 +1,144 @@+{- |+Module      :  Data.LTS+Description :  A library that models labelled transition system in Haskell+Copyright   :  Copyright (c) 2020 Ajay Kumar Eeralla++Maintainer  :  ajay.eeralla@gmail.com+Stability   :  experimental+Portability :  portable++This module implements a labelled transition system+-}+{-# LANGUAGE DeriveGeneric #-}++module Data.LTS+  ( LTSState (..)+  , Transition (..)+  , LTS+  , checkTrans+  , getFromIds+  , getToIds+  , sortById+  , sortByToSt+  , sortByFromSt+  , collectTrans+  , getStartSt+  , getFinalSt+  , depth+  , Alphabet+  , findTransIndex+  , transExists+  )+where+import Data.Nat+import GHC.Generics+import Data.List (sortBy)+import Data.Ord (comparing)++-- | LTSState is a record type which may hold id, output, etc.+data LTSState a =+  LTSState {stateId::Int+           , out::a+           }+           deriving (Read, Show, Eq, Generic)++-- | Define Ord instance by id+instance (Eq a) => Ord (LTSState a) where+  compare = comparing stateId++-- | Transition models that on a LTSState, given input symbol from an alphabet [b],+-- | takes to the next LTSState+data Transition a b =+  Transition { transitionFrom::LTSState a+             , transitionGuard::b+             , transitionTo::LTSState a+             }+             deriving (Read, Show, Eq, Generic)++-- | Define Ord instance for `Transition`+instance (Eq a, Eq b) => Ord (Transition a b) where+  compare = comparing transitionFrom++-- | Alphabet is a generic list+type Alphabet b = [b]++-- | LTS is a list of `Transition`+type LTS a b = [Transition a b]++-- | Check if transition exists from a given symbol from `Alphabet` and `LTSState`+transExists :: (Eq a, Eq b) => LTSState a -> b -> LTS a b -> Bool+transExists st x (t:ts) =+  (transitionFrom t == st && transitionGuard t == x) || transExists st x ts++-- | Return the index of the `Transition` that current state can take on input symbol+findTransIndex :: (Eq a, Eq b) => LTSState a -> b -> LTS a b -> Int+findTransIndex st x (t:ts) =+  if transExists st x (t:ts)+    then index+    else error "doesn't exist"+  where index = if transitionFrom t == st && transitionGuard t == x+                then 0+                else 1+ findTransIndex st x ts++-- | Return the next state given the input symbol on current `LTSState`+nextStateSymbol :: (Eq a, Eq b) => LTSState a -> b -> LTS a b -> LTSState a+nextStateSymbol s x ts =+  if transExists s x ts+    then transitionTo (ts !! findTransIndex s x ts)+    else s++-- | LTS execution on a given state and `Alphabet`+nextStateAlphabet :: (Eq a, Eq b) => LTSState a -> Alphabet b -> LTS a b -> LTSState a+nextStateAlphabet s (x:xs) ts =+  nextStateAlphabet (nextStateSymbol s x ts) xs ts++-- | Check if the set of transitions has same origin+checkTrans :: (Eq a, Eq b) => LTSState a -> LTS a b -> Bool+checkTrans st (t:ts) =+  stateId st == stateId (transitionFrom t) && checkTrans st  ts++-- | Sorting related functions+-- | Get origin `LTSState` ids+getFromIds:: (Eq a, Eq b) =>  LTS a b -> [Int]+getFromIds = map (stateId . transitionFrom)++-- | Get final `LTSState` ids+getToIds :: (Eq a, Eq b) => LTS a b -> [Int]+getToIds = map (stateId . transitionTo)++-- | Sort `LTSState`s by Id+sortById :: (Eq a) => [LTSState a] -> [LTSState a]+sortById = sortBy (comparing stateId)++-- | Sort transitions by from `LTSState`+sortByFromSt :: (Eq a, Eq b) => LTS a b -> LTS a b+sortByFromSt = sortBy (comparing transitionFrom)++-- | Sort transitions by to `LTSState`+sortByToSt :: (Eq a, Eq b) => LTS a b -> LTS a b+sortByToSt = sortBy (comparing transitionTo)++-- | Compute set of transitions (that can be ordered using a flag b) from a given `LTSState`+collectTrans:: (Eq a, Eq b) => LTSState a  -> LTS a b -> Bool -> LTS a b+collectTrans st (t:ts) b =+  let op = if stateId st == stateId (transitionFrom t)+              then t:collectTrans st ts b+              else collectTrans st ts b+  in if b then sortByToSt op else op++-- | Get the start `LTSState`+getStartSt :: (Eq a, Eq b) => LTS a b -> LTSState a+getStartSt ts =  transitionFrom (head (sortByToSt (sortByFromSt ts)))++-- | Get the final `LTSState`+getFinalSt :: (Eq a, Eq b) => LTS a b -> LTSState a+getFinalSt ts =  transitionTo (head (sortByToSt (sortByFromSt ts)))++-- | Compute depth of a transition system which is the longest simple path+-- | from the start state to a final state+depth :: (Eq a, Eq b) => LTS a b -> LTSState a -> Nat+depth [] _ = 0+depth (t:ts) st+  | transitionFrom t == st && (transitionFrom t /= transitionTo t) =+    1 + depth ts (transitionTo t)+  | otherwise = depth ts st

+ tests/Main.hs view

@@ -0,0 +1,45 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module Main+where+import Test.Tasty+import Test.Tasty.SmallCheck as SC+import Test.Tasty.HUnit+import Data.LTS+import GHC.Generics+import Test.SmallCheck.Series+++main = defaultMain tests++tests :: TestTree+tests = testGroup "Tests" [properties, unitTests]++properties :: TestTree+properties = testGroup "Properties" [scProps]++instance Serial m a => Serial m (LTSState a)+instance (Serial m a, Serial m b) => Serial m (Transition a b)++scProps = testGroup "(checked by SmallCheck)"+    [ SC.testProperty "sortById == sortById . sortById" $+      \xs -> sortById (xs :: [LTSState Int]) == sortById (sortById xs)+    ]++s0 :: LTSState Int = LTSState {stateId=0, out=3}+s1 :: LTSState Int = LTSState {stateId=1, out=5}+s2 :: LTSState Int = LTSState {stateId=2, out=7}+t1 :: Transition Int Char = Transition {transitionFrom=s0, transitionGuard='a', transitionTo=s1}+t2 :: Transition Int Char = Transition {transitionFrom=s1, transitionGuard='b', transitionTo=s2}++unitTests = testGroup "Unit tests"+  [ testCase "Depth comparison" $+      depth [t1, t2] s0 `compare` 2 @?= EQ+  , testCase "Compare transition index" $+      findTransIndex s0 'a' [t1, t2] `compare` 1 @?= LT+  , testCase "Check transition Exists" $+      transExists s1 'b' [t1, t2] `compare` True @?= EQ+  ]