Coder Social home page Coder Social logo

petercfontana / timesolver Goto Github PK

View Code? Open in Web Editor NEW

This project forked from jkeiren/timesolver

0.0 0.0 0.0 64.93 MB

On-the-fly model checker for timed automata with support for the alternation-free modal mu-calculus.

License: MIT License

CMake 2.34% Python 4.24% C++ 82.54% Shell 0.83% TeX 1.65% Lex 1.06% Yacc 7.34%

timesolver's Introduction

TimeSolver

This program is a Model Checker for timed automata that uses pes (predicate equation systems).

Contents

Authors

Written by Peter Fontana ([email protected]), Rance Cleaveland ([email protected]) Jeroen Keiren ([email protected]). Based on earlier work by Dezhuang Zhang.

Getting the source

You can obtain the source of the development version from Bitbucket:

[email protected]:jkeiren/TimeSolver.git

Installing/Compiling

The build system uses CMake. The minimal required version is CMake 3.5. If you want to be able to generate Doxygen documentation, you should use version 3.9 or newer. If you want to be able to run the unit tests, version 3.10 is required.

Building

To build, execute the following from the root of your working copy.

mkdir build
cd build
cmake ..
make

This will create a default build of timesolver. If you want to use multiple threads when building, use make -jN with N the number of threads.

Installing

You can install the tool by executing, from the build directory

make install

By default, this will install to /usr/local/bin. If you want to install to another location, execute the following from your build directory before make install (or when executing the intial cmake command)

cmake .. -DCMAKE_INSTALL_PREFIX=/path/to/prefix

Cleaning

If you followed the instructions above, you can clean up by doing rm -r build from the root of your repository.

Generating source code documentation

You can generate source code documentation using make doxygen. The output will be generated in the directory build/pes.timed/html.

Dependencies

No additional libraries are needed. For testing, googletest is used, but this is downloaded on-demand.

Testing

Unit tests and tool tests are included in the build system. All tests can be run from the build directory in which you built the tool, by executing

ctest -jN

where N is again the number of threads to execute.

If you only want to run the examples, you can use

ctest -jN -R tooltest

If you want to run all but the tooltests (i.e. the unit tests), you can use

ctest -jN -E tooltest

Running the Program

The executable program is named timesolver-ta.

To run, use timesolver-ta <exampleFile>

Example files are included in the example directory.

Program Outputs

The program will output whetehr the formula is vaild or invalid, with the running time. Furthermore, a simple vacuity is implemented. This program will also identify any unchecked subformulas. This provides a sound but incomplete vacuity checking for the formula. We know that any subformula not examined during the proof does not affect the truth of the formula (soundness), however it may check subformula it does not need to check (incompleteness). The prover checks subformula from left to right.

To see the entire proof, enable the -d option.

Generating Examples

This section is outdated, and needs to be updated.

Running ./build_all.sh will compile the program and the example-generating programs.

Most examples are already there. Some are program-generated. To compile the programs to generate examples, either run "make" in each directory (with the desired makefile), or in the regular directory run ./build_all.sh This will compile the original program and the example-generating programs.

Then, run each program and provide as a parameter the number of processes. This will then write to standard output the generated example. It is recommended to redirect the output to a file.

Some folders will have various examples.

Notes

No additional Notes.

timesolver's People

Contributors

jkeiren avatar petercfontana avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.