Ymer extended to adaptive sampling
C++ C HTML Shell Python Perl 6 Other
Clone or download
Pull request Compare This branch is 1 commit ahead, 17 commits behind hlsyounes:master.
Permalink
Failed to load latest commit information.
cudd Normalize rate matrix in DecisionDiagramModel for DTMC, so that it re… Feb 18, 2015
dcmt Update to latest version of Dynamic Creator library for creating para… Oct 23, 2012
examples Added adaptive simulation engine. May 21, 2015
glog Add .gitignore config files. Apr 28, 2015
gsl Prepare version 4.2.1 for release. Apr 30, 2015
gtest Add .gitignore config files. Apr 28, 2015
m4 Replace symbolic links with copies of m4 files. May 2, 2015
scripts Merge changes to 3.0 release branch back into trunk. Apr 10, 2012
src Added adaptive simulation engine. May 21, 2015
.gitignore Add .gitignore config files. Apr 28, 2015
AUTHORS Update AUTHORS. Feb 18, 2015
COPYING Initial revision Nov 7, 2003
ChangeLog Reset trunk to 3.0. Apr 10, 2012
INSTALL Reset trunk to 3.0. Apr 10, 2012
Makefile.am Move decision diagram model to src dir and add simple test. Apr 1, 2015
Makefile.in Move decision diagram model to src dir and add simple test. Apr 1, 2015
NEWS Prepare version 4.2.1 for release. Apr 30, 2015
README Prepare version 4.2.1 for release. Apr 30, 2015
aclocal.m4 Update to autoconf 1.69 and automake 1.14.1. Add compiled OR and IFF … Sep 24, 2014
comm.h Switch to C++11. Use enum class for Type enum. Aug 31, 2012
compile Update to autoconf 1.69 and automake 1.14.1. Add compiled OR and IFF … Sep 24, 2014
config.guess Merge changes to 3.0 release branch back into trunk. Apr 10, 2012
config.h.in Merge changes to 3.0 release branch back into trunk. Apr 10, 2012
config.sub Merge changes to 3.0 release branch back into trunk. Apr 10, 2012
configure Prepare version 4.2.1 for release. Apr 30, 2015
configure.ac Prepare version 4.2.1 for release. Apr 30, 2015
depcomp Merge changes to 3.0 release branch back into trunk. Apr 10, 2012
experiments_reach.sh Added adaptive simulation engine. May 21, 2015
formulas.h Add more statistics for sample path lengths. Closes #24. May 9, 2015
hybrid.cc Re-implement ODD construction in ddutil library. New construction wor… Jan 2, 2015
hybrid.h Re-implement ODD construction in ddutil library. New construction wor… Jan 2, 2015
install-sh Merge changes to 3.0 release branch back into trunk. Apr 10, 2012
ltmain.sh Replace symbolic link for ltmain.sh with real file. May 3, 2015
missing Merge changes to 3.0 release branch back into trunk. Apr 10, 2012
mkinstalldirs Merge changes to 3.0 release branch back into trunk. Apr 10, 2012
sampling.cc Added adaptive simulation engine. May 21, 2015
symbolic.cc Support multiple initial states for the hybrid engine. Apr 3, 2015
test-driver Update to autoconf 1.69 and automake 1.14.1. Add compiled OR and IFF … Sep 24, 2014
ylwrap Merge changes to 3.0 release branch back into trunk. Apr 10, 2012
ymer.cc Added adaptive simulation engine. May 21, 2015

README

Copyright (C) 2003--2005 Carnegie Mellon University
Copyright (C) 2011-2015 Google Inc

   This file is free documentation; the copyright holders give
unlimited permission to copy, distribute and modify it.

Ymer 4.2.1
==========

Ymer is a tool for verifying probabilistic properties of discrete-time Markov
chains (DTMCs), continuous-time Markov chains (CTMCs) and generalized
semi-Markov processes (GSMPs).  Properties are expressed using the Continuous
Stochastic Logic (CSL).

To handle the full generality of GSMPs, Ymer implements statistical techniques,
based on discrete event simulation and sequential acceptance sampling, for CSL
model checking.  Ymer includes support for distributed acceptance sampling,
i.e. the use of multiple machines to generate samples, which can result in
significant speedup as each sample can be generated independently.

Ymer can also use numerical techniques based on uniformization by approximating
a GSMP with a CTMC using phase-type distributions.  Ymer includes the hybrid
engine from the PRISM tool for CTMC model checking.  Numerical and statistical
techniques can be used in combination to solve nested CSL queries.


Installation
============

Installation instructions are available in INSTALL.


Running Ymer
============

Ymer is controlled by a command line interface.  Run `./ymer --help' for details
on available command line options.


Distributed Sampling
====================

To start Ymer in server mode, provide a port with the command line options.  The
server will accept connections from clients, which will provide the server with
samples.  To connect a client to a server, pass a host name and a port to Ymer.
The following commands give you an example of how to use distributed sampling
with Ymer:

  cpu1> ymer -P 5000 examples/tandem63.sm examples/tandem500.csl

  cpu2> ymer -H cpu1 -P 5000 examples/tandem63.sm examples/tandem500.csl

  cpu3> ymer -H cpu1 -P 5000 examples/tandem63.sm examples/tandem500.csl

This starts a server on a machine called `cpu1' and a client on each of the
machines called `cpu2' and `cpu3'.  Once enough samples have been generated, the
server terminates, which in turn causes the clients to terminate as well.

Using ssh, for example, it is possible to write a script that will start a
server locally and a set of clients on remote machines.  An example of such a
script is `scripts/ymer-dist2', which runs a server on the local machine and two
sample generating clients on two machines named `sweden' and `gs222'.

Note that the model and property files must be available on all machines running
Ymer.  The behavior of Ymer is unspecified if a client uses a different model or
property than the server it connects to.