From 055be8d0d9a72634b63fa8b1e820607785e66084 Mon Sep 17 00:00:00 2001 From: Hans-Peter Deifel <hpd@hpdeifel.de> Date: Fri, 16 Nov 2018 17:35:11 +0100 Subject: [PATCH] prism: Fix pdf export --- prism/benchmark.org | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/prism/benchmark.org b/prism/benchmark.org index 80cc557..64c0e99 100644 --- a/prism/benchmark.org +++ b/prism/benchmark.org @@ -1,4 +1,5 @@ #+TITLE: PRISM Benchmarks +#+LATEX_HEADER: \usepackage[a4paper,margin=1in,landscape]{geometry} * Introduction @@ -1190,7 +1191,7 @@ We consider the scenario where two stations trying to send packets simultaneously. The PRISM model is taken from [KNS02a] using the integer semantics given in [KNS06]. In the model one time unit - corresponds to 50μs and to ensure integer bounds, where neccessary, scaling lower bound constraints down and + corresponds to 50\mu s and to ensure integer bounds, where neccessary, scaling lower bound constraints down and upper bound constraints up to sensure a sound abstraction. For more information on the probabilistic timed automata see: http://www.prismmodelchecker.org/casestudies/wlan.php -- GitLab