From 4db7afeac702923857f802e369fd73ffc264c45b Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 22 Sep 2019 18:47:28 +0100
Subject: [PATCH] Added some details on running the examples

---
 README.md | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/README.md b/README.md
index 82636e6..18fc5c9 100644
--- a/README.md
+++ b/README.md
@@ -6,3 +6,21 @@ The toolkit consists of two separate modules implementing:
 * BDD-based methods
 * SMT-based methods
 
+## Example
+
+The `examples` directory contains sample input files.
+
+To quickly the BDD module you can perform verification of the TGC controller consiting of three trains:
+
+```
+$ ./reactics bdd -c f1 examples/bdd/tgc.rs
+```
+
+The above command tests the formula labelled `f1` in the input file.
+
+To test the SMT module you can perform reachability verification of the scalable chain system:
+
+```
+$ ./reactics smt examples/smt/chain_reaction.py 2 3 1
+```
+