Merge branch 'mcrl2-converter'

  default-language:    Haskell2010

  ghc-options:         -Wall

executable prism-converter

  hs-source-dirs:      src/prism-converter

  main-is:             Main.hs

  other-modules:       Parser

library prism-converter-lib

  hs-source-dirs:      src/prism-converter/lib

  exposed-modules:     Parser

                     , MarkovChain

                     , Mdp

                     , Mdp.Types

                     , StatesFile

                     , Mdp.Mcrl2

  default-language:    Haskell2010

  build-depends:       base >= 4.11

                     , text

                     , vector

                     , megaparsec >= 7

                     , containers

                     , optparse-applicative

                     , prettyprinter

                     , prettyprinter-ansi-terminal

                     , prettyprinter-convert-ansi-wl-pprint

                     , microlens

                     , microlens-th

                     , microlens-platform

                     , containers ^>= 0.6

                     , megaparsec ^>= 7

                     , microlens ^>= 0.4.10

                     , microlens-platform ^>= 0.3.11

                     , microlens-th ^>= 0.4.2

                     , text ^>= 1.2.3

                     , vector ^>= 0.12

                     , vector-algorithms ^>= 0.8.0.1

  ghc-options:         -Wall -Wno-name-shadowing

  if !flag(benchmark-generators)

    buildable:       False

executable prism-converter

  hs-source-dirs:      src/prism-converter

  main-is:             Main.hs

  default-language:    Haskell2010

  build-depends:       base >= 4.11

                     , prism-converter-lib

                     , containers ^>= 0.6

                     , megaparsec ^>= 7

                     , optparse-applicative ^>= 0.14.3

                     , prettyprinter ^>= 1.2 || ^>= 1.3

                     , prettyprinter-ansi-terminal ^>= 1.1

                     , prettyprinter-convert-ansi-wl-pprint ^>= 1.1

                     , text ^>= 1.2.3

  ghc-options:         -Wall -Wno-name-shadowing

  if !flag(benchmark-generators)

    buildable:       False

test-suite prism-converter-tests

  type:                exitcode-stdio-1.0

  hs-source-dirs:      src/prism-converter

  main-is:             Tests.hs

  default-language:    Haskell2010

  build-depends:       base >= 4.11

                     , hspec >= 2.6 && <2.8

                     , microlens-platform ^>= 0.3.11

                     , prism-converter-lib

                     , vector ^>= 0.12.0.2

                     , text ^>= 1.2.3

  ghc-options:         -Wall -Wno-name-shadowing

  if !flag(benchmark-generators)

    buildable:       False

{-# LANGUAGE OverloadedStrings #-}

{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE TupleSections #-}

{-# LANGUAGE TypeApplications #-}

module Main (main) where

import           System.IO

import           System.Exit

import           Data.Semigroup

import           Control.Applicative

import           Data.Maybe (fromMaybe)

import           Data.Set (Set)

import qualified Data.Set as S

import           Data.Text (Text)

import qualified Data.Text as T

import qualified Data.Text.IO as T

  show CTMC = "ctmc"

  show MDP = "mdp"

data OutputFormat = Valmari | Valmari2 | Copar

data OutputFormat = Valmari | Valmari2 | Copar | Mcrl2

instance Show OutputFormat where

  show Valmari = "valmari"

  show Valmari2 = "valmari2"

  show Copar = "copar"

  show Mcrl2 = "mcrl2"

parseOutputFormat :: String -> Either String OutputFormat

parseOutputFormat "valmari" = Right Valmari

parseOutputFormat "valmari2" = Right Valmari2

parseOutputFormat "copar" = Right Copar

parseOutputFormat "mcrl2" = Right Mcrl2

parseOutputFormat other = Left ("Unknown output format '" <> other <> "'")

data Options = Options

     (OptParse.eitherReader parseOutputFormat)

     (OptParse.long "output-format" <>

      OptParse.help

        "Syntax used for the output file. Can be either 'copar', 'valmari' or 'valmari2'" <>

        "Syntax used for the output file. Can be either 'copar', 'valmari', 'valmari2' or 'mcrl2'" <>

      OptParse.metavar "FORMAT" <>

      OptParse.value Copar <>

      OptParse.showDefault)) <*>

      Left err -> do

        hPutStrLn stderr $ "error while parsing --partition-on-variables: " <> T.unpack err

        exitFailure

      Right vars -> return (Just (computePartition sf vars))

      Right vs -> return (Just (computePartition sf vs))

    _ -> return Nothing

  case (optModelType opts, optOutputFormat opts) of

            Valmari -> valmariMdpB

            Valmari2 -> valmariMdp2B

            Copar -> mdpB

            Mcrl2 -> mcrl2B

      in convert opts mdpP (builder initPartition)

    (inType, outType) ->

      let mcType =

              Valmari -> valmariMarkovChainB

              Valmari2 -> error "valmari2 only implemented for MDPs"

              Copar -> markovChainB

              Mcrl2 -> error "mcrl2-format only supports MDPs"

       in convert opts (markovChainP mcType) (builder initPartition)

# Prism converter

This directory containers a helper program called `prism-converter` that

converts transition matrices of PRISM[1] models into coalgebra specifications.

## Building

```sh

stack build --flag copar:benchmark-generators

```

## Generating transition matrices

You can generate those transition matrices with PRISM itself by using:

```sh

prism -exporttrans TRA_FILE -exportstates STA_FILE -const CONST_ASSIGNMENTS

```

Given the constant assignments `CONST_ASSIGNMENTS` (see the PRISM documentation

on syntax and semantics of those), thsi output a transition matrix in `TRA_FILE`

and a states file in `STA_FILE`. Please see [2] for additional details.

## Converting them into coalgebra specs

The resulting files can then be converted into a coalgebra specification using

```sh

stack exec prism-converter -- --model-type TYPE --states-file STA_FILE TRA_FILE

```

where type is one of dtmc, ctmc or mdp.

See `stack exec prism-converter -- --help` for details.

[1]: https://www.prismmodelchecker.org

[2]: https://www.prismmodelchecker.org/manual/RunningPRISM/ExportingTheModel

{-# LANGUAGE OverloadedStrings #-}

module Main (main) where

import           Lens.Micro.Platform

import           Test.Hspec

import qualified Data.Vector                   as V

import qualified Data.Text.Lazy.Builder        as Build

import Mdp.Mcrl2

import Mdp.Types

import StatesFile

main :: IO ()

main = hspec $ do

  convertToMcrlSpec

  mcrl2BSpec

convertToMcrlSpec :: Spec

convertToMcrlSpec = describe "convertToMcrl" $ do

  it "generates the correct number of states" $ do

    let mdp = Mdp 4 1 mempty

    let res = convertToMcrl Nothing mdp

    res ^. numStates `shouldBe` mdp ^. numStates

  it "generates a uniform initial distribution" $ do

    let mdp = Mdp 4 1 mempty

    let res = convertToMcrl Nothing mdp

    res ^.. outDistribution . each . probability `shouldBe` (replicate 4 0.25)

  it "generates the correct transition if there's only one" $ do

    let mdp = Mdp 2 1 (V.singleton (Transition 0 0 1 1.0 Nothing))

    let res = convertToMcrl Nothing mdp

    let trans = Mcrl2Transition 0 "0" (V.singleton (Mcrl2PropTrans 1.0 1))

    res ^? transitions . ix 0 `shouldBe` Just trans

  it "generates one out-distribution for two transitions with same label" $ do

    let mdp = Mdp 2 1 (V.fromList [Transition 0 0 0 0.5 Nothing, Transition 0 0 1 0.5 Nothing])

    let res = convertToMcrl Nothing mdp

    let trans = Mcrl2Transition 0 "0" (V.fromList [Mcrl2PropTrans 0.5 0, Mcrl2PropTrans 0.5 1])

    res ^? transitions . ix 0 `shouldBe` Just trans

  it "groups non-consecutive transitions with same source and label" $ do

    let mdp = Mdp 2 1 (V.fromList [Transition 0 0 0 0.5 Nothing

                                  , Transition 0 1 1 1.0 Nothing

                                  , Transition 0 0 1 0.5 Nothing])

    let res = convertToMcrl Nothing mdp

    let trans = [ Mcrl2Transition 0 "0" (V.fromList [Mcrl2PropTrans 0.5 0, Mcrl2PropTrans 0.5 1])

                , Mcrl2Transition 0 "1" (V.fromList [Mcrl2PropTrans 1.0 1])

                ]

    res ^.. transitions . each `shouldBe` trans

  it "generates two two distinct transitions for two transitions with different label" $ do

    let mdp = Mdp 2 2 (V.fromList [Transition 0 0 1 1.0 Nothing, Transition 0 1 1 1.0 Nothing])

    let res = convertToMcrl Nothing mdp

    let trans1 = Mcrl2Transition 0 "0" (V.singleton (Mcrl2PropTrans 1.0 1))

    let trans2 = Mcrl2Transition 0 "1" (V.singleton (Mcrl2PropTrans 1.0 1))

    res ^.. transitions . traverse `shouldBe` [trans1, trans2]

  it "correctly models the initial partition" $ do

    let mdp = Mdp 2 2 (V.fromList [Transition 0 0 1 1.0 Nothing, Transition 0 1 1 1.0 Nothing])

    let part = Partition 2 (V.fromList [0, 1])

    let res = convertToMcrl (Just part) mdp

    let trans = [ Mcrl2Transition 0 "0" (V.singleton (Mcrl2PropTrans 1.0 1))

                , Mcrl2Transition 0 "1" (V.singleton (Mcrl2PropTrans 1.0 1))

                , Mcrl2Transition 2 "i0" (V.singleton (Mcrl2PropTrans 1.0 0))

                , Mcrl2Transition 3 "i1" (V.singleton (Mcrl2PropTrans 1.0 1))

                ]

    res ^.. transitions . traverse `shouldBe` trans

mcrl2BSpec :: Spec

mcrl2BSpec = describe "mcrl2BSpec" $ do

  it "works for an example" $ do

    let mdp = Mdp 2 2 (V.fromList [Transition 0 0 1 1.0 Nothing, Transition 0 1 1 1.0 Nothing])

    let res = "des (0 1/2 1,2,2)\n(0,\"0\",1)\n(0,\"1\",1)\n"

    (Build.toLazyText (mcrl2B (convertToMcrl Nothing mdp)) ^. strict) `shouldBe` res

  it "works for another example" $ do

    let mdp = Mdp 2 1 (V.fromList [Transition 0 0 0 0.5 Nothing, Transition 0 0 1 0.5 Nothing])

    let res = "des (0 1/2 1,1,2)\n(0,\"0\",0 1/2 1)\n"

    (Build.toLazyText (mcrl2B (convertToMcrl Nothing mdp)) ^. strict) `shouldBe` res

  it "works for an example with initial partition" $ do

    let mdp = Mdp 2 2 (V.fromList [Transition 0 0 1 1.0 Nothing, Transition 0 1 1 1.0 Nothing])

    let part = Partition 2 (V.fromList [0, 1])

    let res = "des (0 1/4 1 1/4 2 1/4 3,4,4)\n(0,\"0\",1)\n(0,\"1\",1)\n(2,\"i0\",0)\n(3,\"i1\",1)\n"

    (Build.toLazyText (mcrl2B (convertToMcrl (Just part) mdp)) ^. strict) `shouldBe` res