From d957aca9badac12180f9b5657b8618d567a67420 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hajdu=20=C3=81kos?= Date: Wed, 13 Sep 2017 17:38:50 +0200 Subject: [PATCH] Updated readme files --- README.md | 18 ++++++++++++++++-- doc/For-developers.md | 3 --- doc/README.md | 8 -------- 3 files changed, 16 insertions(+), 13 deletions(-) delete mode 100644 doc/README.md diff --git a/README.md b/README.md index 2e2c23ed38..c7c48521c5 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,21 @@ [![Build Status](https://travis-ci.com/FTSRG/theta-dev.svg?token=85GYo3nhkE5uMJYayyw8&branch=master)](https://travis-ci.com/FTSRG/theta-dev) +## About + _Theta_ is a generic, modular and configurable model checking framework developed at the [Fault Tolerant Systems Research Group](http://inf.mit.bme.hu/en) of [Budapest University of Technology and Economics](http://www.bme.hu/?language=en), aiming to support the design and evaluation of abstraction refinement-based algorithms for the reachability analysis of various formalisms. -The main distinguishing characteristic of Theta is its architecture that allows the definition of input formalisms with higher level language front-ends, and the combination of various abstract domains, interpreters, and strategies for abstraction and refinement. +The main distinguishing characteristic of Theta is its architecture that allows the definition of input formalisms with higher level language front-ends, and the combination of various abstract domains, interpreters, and strategies for abstraction and refinement. If you want to read more, take a look at the [list of publications](http://home.mit.bme.hu/~hajdua/theta/). + +## Get Theta + +* Clone the repository. +* Build the projects from the command line by executing `gradlew.bat build` (Windows) or `./gradlew build` (Linux) from the root directory. +* On Windows, some libraries are required from the [Microsoft Visual C++ Redistributable package](https://www.microsoft.com/en-us/download/details.aspx?id=48145). Install it, or just go into the `lib` folder and execute `Download-VCredist.ps1`, which will download the required libraries. + +## Use Theta + +If you want to use the existing algorithms and tools defined in Theta, then take look at [doc/Tools.md](doc/Tools.md). + +## Extend Theta -For more information, see the [list of publications](http://home.mit.bme.hu/~hajdua/theta/) and the [doc](doc) folder. +If you want to extend Theta and build your own algorithms and tools, then take look at [doc/For-developers.md](doc/For-developers.md), [doc/Architecture.md](doc/Architecture.md) and [Coding-conventions.md](doc/Coding-conventions.md). diff --git a/doc/For-developers.md b/doc/For-developers.md index 448df2f612..70ae042463 100644 --- a/doc/For-developers.md +++ b/doc/For-developers.md @@ -8,9 +8,6 @@ As the main repository is read-only, we suggest you to create your own [fork](ht As the framework is under development, we suggest you to [sync your fork](https://help.github.com/articles/syncing-a-fork/) often and merge the master branch into your development branch(es). -## Building from the command line -Thanks to the Gradle Wrapper, no installation is required. The projects can be simply built from the command line by executing `gradlew.bat build` (Windows) or `./gradlew build` (Linux) from the root directory. - ## Importing and developing in Eclipse The projects are currently developed and tested with [Oxygen](https://www.eclipse.org/oxygen/). diff --git a/doc/README.md b/doc/README.md deleted file mode 100644 index b0c1b34faf..0000000000 --- a/doc/README.md +++ /dev/null @@ -1,8 +0,0 @@ -# Information - -Theta is a generic, modular and configurable model checking framework providing: - -* **Formalisms** to describe software/hardware systems, e.g., symbolic transition systems, timed automata, control flow automata. -* **Algorithms** for the verification of formalisms, e.g., CEGAR-based reachability analysis. - -If you want to use the existing algorithms and tools defined in Theta, then take look at [Tools.md](Tools.md). If you want to extend Theta and build your own algorithms and tools, then take look at [For-developers.md](For-developers.md), [Architecture.md](Architecture.md) and [Coding-conventions.md](Coding-conventions.md). \ No newline at end of file