inmathwetrust / dwina Goto Github PK
View Code? Open in Web Editor NEWThis project forked from tfiedor/dwina
Implementation of decision procedure for WSkS logic
This project forked from tfiedor/dwina
Implementation of decision procedure for WSkS logic
** * dWiNA - Deciding WSkS using non-deterministic automata * * Copyright (c) 2014 Tomas Fiedor <[email protected]> ************************************************************** * About * ********* dWiNA is an implementation of backward decision procedure for WSkS logic (weak second-order theory of k successors). The tool is using libvata a highly optimised non-deterministic finite tree automata library that supports semi-symbolic encoding using multi-terminal binary decision diagrams (MTBDDs) for storing transition table of the automaton. Procedure generates state space on-the-fly and prunes the states using the antichain-based approach. State space is represented by downward and upward closed represenation of states. The tool computes the representation of final states and test if initial states are included in final states and thus (dis)prove validity. * Prerequisities * ****************** Following packages are needed in order to compile and run dWiNA on your system: git (>= 1.6.0.0) cmake (>= 2.8.2) gcc (>= 4.8.0) flex (>= 2.5.35) bison (>= 2.7.1) * Download * ************ In order to compile and work with our tool we highly recommend to clone the repository to the local repository. You need to have the git version control system installed. To download the library, run $ git clone https://github.com/Raph-Stash/dWiNA.git * Compilation * *************** In order to prepare the tool for compilation and commiting a background check for prerequisite package issue the following command in the root directory of the tool: $ cmake CMakeLists.txt To further compile the source files to runable binary issue the following command: $ make * Input file syntax * ********************* The following grammar describes supported subset of MONA syntax for the specification of verified formulae. It uses the classical BNF-like notation. For full syntax for MONA tool consult the tool manual at http://www.brics.dk/mona/mona14.pdf. program ::= (header;)? (declaration;)+ header ::= ws1s | ws2s declaration ::= formula | var0 (varname)+ | var1 (varname)+ | var2 (varname)+ | 'pred' varname (params)? = formula | 'macro' varname (params)? = formula formula ::= 'true' | 'false' | (formula) | zero-order-var | ~formula | formula | formula | formula & formula | formula => formula | formula <=> formula | first-order-term = first-order-term | first-order-term ~= first-order-term | first-order-term < first-order-term | first-order-term > first-order-term | first-order-term <= first-order-term | first-order-term >= first-order-term | second-order-term = second-order-term | second-order-term = { (int)+ } | second-order-term ~= second-order-term | second-order-term 'sub' second-order-term | first-order-term 'in' second-order-term | ex1 (varname)+ : formula | all1 (varname)+ : formula | ex2 (varname)+ : formula | all2 (varname)+ : formula first-order-term ::= varname | (first-order-term) | int | first-order-term + int second-order-term ::= varname | (second-order-term) | second-order-term + int * Contact * *********** If you have any questions, do not hesitate to contact the tool/method authors: * Tomas Fiedor <[email protected]> (corresponding author of dWiNA) * Ondrej Lengal <[email protected]> (corresponding author of VATA) * Lukas Holik <[email protected]> * Tomas Vojnar <[email protected]>
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.