Skip to content
Snippets Groups Projects
Commit 055be8d0 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel
Browse files

prism: Fix pdf export

parent fd8af0d1
No related branches found
No related tags found
No related merge requests found
#+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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment