Commit 1b10d875 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel 🐢
Browse files

Add mcrl2 as output format to main

parent eb15e479

src/prism-converter/Main.hs

+7 −7
Original line number Diff line number Diff line
@@ -36,17 +36,19 @@ instance Show ModelType where 
  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
@@ -99,7 +101,7 @@ optionsParser = 
     (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)) <*>
@@ -170,7 +172,8 @@ main = do 
            Valmari -> valmariMdpB

            Valmari2 -> valmariMdp2B

            Copar -> mdpB

      in convert opts (alien (fromRational @Double) $ mdpP) (builder initPartition)

            Mcrl2 -> mcrl2B

      in convert opts mdpP (builder initPartition)

    (inType, outType) ->

      let mcType =

            case inType of
@@ -181,8 +184,5 @@ main = do 
              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)
 




alien :: (Functor f, Functor g) => (a -> b) -> f (g a) -> f (g b)

alien = ((<$>) . (<$>))

src/prism-converter/lib/Mdp.hs

+20 −9
Original line number Diff line number Diff line
@@ -5,6 +5,7 @@ 
{-# LANGUAGE OverloadedStrings #-}

{-# LANGUAGE TemplateHaskell #-}

{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE TypeApplications #-}



module Mdp (mdpP, mdpB, valmariMdpB, valmariMdp2B, mcrl2B) where
@@ -27,6 +28,13 @@ import Parser 
import           StatesFile                     ( Partition(..) )

import qualified Mdp.Mcrl2                     as Mcrl2



----------------------------------------------------------------------

-- helpers

----------------------------------------------------------------------



convertToDouble :: Mdp Rational -> Mdp Double

convertToDouble = fmap (fromRational @Double)



----------------------------------------------------------------------

-- Parser

----------------------------------------------------------------------
@@ -52,9 +60,10 @@ transitionP = 
-- Builder

----------------------------------------------------------------------



mdpB :: Maybe Partition -> (Mdp Double) -> Build.Builder

mdpB :: Maybe Partition -> (Mdp Rational) -> Build.Builder

mdpB partition mdp =

  functorB partition <> "\n" <> transitionsB partition (mdp ^. transitions)

  let mdp' = convertToDouble mdp

  in functorB partition <> "\n" <> transitionsB partition (mdp' ^. transitions)



functorB :: Maybe Partition -> Build.Builder

functorB Nothing = "P(Nx(DX))\n"
@@ -241,15 +250,15 @@ partToBlocks p = 
  in  M.elems blockMap





valmariMdpB :: Maybe Partition -> (Mdp Double) -> Build.Builder

valmariMdpB :: Maybe Partition -> (Mdp Rational) -> Build.Builder

valmariMdpB partition mdp =

  let (vmdp, vpartition) = convertToValmari partition mdp

  let (vmdp, vpartition) = convertToValmari partition (convertToDouble mdp)

  in  valmariMdpBImpl vmdp vpartition





valmariMdp2B :: Maybe Partition -> (Mdp Double) -> Build.Builder

valmariMdp2B :: Maybe Partition -> (Mdp Rational) -> Build.Builder

valmariMdp2B partition mdp =

  let (vmdp, vpartition) = convertToValmari2 partition mdp

  let (vmdp, vpartition) = convertToValmari2 partition (convertToDouble mdp)

  in  valmariMdpBImpl vmdp vpartition
@@ -324,7 +333,9 @@ valmariBlocks part = 
-- mcrl2

----------------------------------------------------------------------



-- TODO Support partition

-- FIXME Support partition



mcrl2B :: Maybe Partition -> Mdp Rational -> Build.Builder

mcrl2B _ = Mcrl2.mcrl2B . Mcrl2.convertToMcrl



mcrl2B :: Mdp Rational -> Build.Builder

mcrl2B = Mcrl2.mcrl2B . Mcrl2.convertToMcrl