diff --git a/prism/benchmark.org b/prism/benchmark.org index 9ae6742e9a1660fbfa618d4123d6dbc990abe02a..edc4d631848f58f715001ddc4d30703014a63563 100644 --- a/prism/benchmark.org +++ b/prism/benchmark.org @@ -244,11 +244,14 @@ path, const_assignments = replace_consts_in_path(model['path'], const_assignments) path_with_consts = const_base_path(path, const_assignments) valmari_file = open(path_with_consts + ".valmari") - out = subprocess.run(['perf', 'stat', config['valmari_cmd']], - stdin=valmari_file, stdout=subprocess.DEVNULL, - stderr=subprocess.PIPE, env={'LC_ALL': 'C'}) - m = re.search(r'(\d+.\d+)\W+seconds time elapsed', out.stderr.decode('utf-8')) - return m[1] + perf = subprocess.Popen(['perf', 'stat', config['valmari_cmd']], + stdin=valmari_file, stdout=subprocess.PIPE, + stderr=subprocess.PIPE, env={'LC_ALL': 'C'}) + sort1 = subprocess.run(['runhaskell', 'valmari-extract-sort1.hs', model['type']], + stdin=perf.stdout, stdout=subprocess.PIPE) + (_, out) = perf.communicate() + m = re.search(r'(\d+.\d+)\W+seconds time elapsed', out.decode('utf-8')) + return (m[1], sort1.stdout.decode('utf-8').strip()) def run_all_valmari(name, const_assignments, initial_partition): convert_model_valmari(name, const_assignments, initial_partition) @@ -267,15 +270,17 @@ stats['explicit-states'], stats['initial-partition-size'], stats['final-partition-size'], + stats['explicit-final-partition-size'], stats['overall-duration'], stats['parse-duration'], stats['refine-duration'], - valmari] + valmari[0], + valmari[1]] #+END_SRC #+NAME: bench #+BEGIN_SRC python :session :eval no-export :var table="" :colnames no :hlines yes - [['Model', 'Consts', 'Partition', "States", "Edges", "Sort 0", "I", "Q", 't(s)', 't_p(s)', 't_r(s)', 't_valmari(s)'], None] + \ + [['Model', 'Consts', 'Partition', "States", "Edges", "Sort 0", "I", "Q", 'Q_0', 't(s)', 't_p(s)', 't_r(s)', 't_valmari(s)', 'Q_0v'], None] + \ list(map(lambda t: run_benchmark(t[0], t[1], t[2]), table[2:])) #+END_SRC diff --git a/prism/valmari-extract-sort1.hs b/prism/valmari-extract-sort1.hs new file mode 100644 index 0000000000000000000000000000000000000000..c12caeb9c9d488662f8a9d6e8991cc13bee468e0 --- /dev/null +++ b/prism/valmari-extract-sort1.hs @@ -0,0 +1,55 @@ +-- Usage: +-- +-- mdpmin < input.valmari | runhaskell valmari-extract-sort1.hs mdp +-- +-- This is a small script that extracts the size of sort 1 from the output of +-- the valmari tool for MDPs. + + +-- This exploits the fact that the valmari implementation prints a list of final +-- blocks that are descendants of a corresponding initial block. Since all +-- states that are _not_ in sort 1 share one block initially, we just have to +-- count the final blocks that origin form all other initial blocks. +-- +-- This is particularly easy, since valmari omits the first block from the in- +-- and output. Since the first block is the block of non-sort-1 states in our +-- input, we just have to count all the states in all blocks printed in the +-- outpu. + + +module Main where + +import System.Environment + +-- | Expects the output of valmaris tool, already tokenized on whitespace and +-- returns the number of final blocks that are in sort 1. +-- +-- +-- The input format is essentially: +-- +-- MC ::= <sizes> <l_transitions> <w_transitions> <blocks> +-- <sizes> ::= num_states num_choices num_l_trans num_w_trans num_blocks +-- <l_transitions> ::= <l_transition>* +-- <l_transition> ::= source choice target +-- <w_transitions> ::= <w_transition>* +-- <w_transition> ::= source weight target +-- <blocks> ::= <block>* +-- <block> ::= state* 0 + +extractSort1 :: [String] -> Int +extractSort1 (_ : _ : numLTrans' : numWTrans' : _ : rest) = + let numTrans = read numLTrans' + read numWTrans' + blocks = drop (numTrans * 3) rest -- Drop all the 'from' 'label' 'to' triples + in length (filter (/= "0") blocks) + + +main :: IO () +main = do + args <- getArgs + case args of + ["mdp"] -> do + sort1 <- (extractSort1 . words) <$> getContents + print sort1 + _ -> do + _ <- getContents -- Ignore input if not an mdp + putStrLn "NA"