Skip to content

Latest commit

 

History

History
63 lines (41 loc) · 1.83 KB

README.md

File metadata and controls

63 lines (41 loc) · 1.83 KB
Raw

SAT-SOLVER

This is a solver for the temporal logic's algorithm SAT. It takes a model as an input and it returns the states where the given formula is valid.

Usage

  1. Clone the repository

  2. CD to the folder of the repository and run the command stack setup.

  3. After that, run the command stack build.

  4. Now the executable is ready. In the folder test you will find some model examples you can use.

  5. To execute, run in your terminal the following command:

    stack exec TP-Final-exe "<path_to_your_file>.sat".

    Make sure the extension of the file is .sat

The grammar.

Syntax

The syntax used to write the CTL formula in the .sat file is pretty simple:

Symbol Translation
TOP ⊤
BT ⊥
! p ¬ p
p & q p ∧ q
p | q p ∨ q
p -> q p → q
AX p ∀◯
EX p ∃◯
A [ p U q ] ∀ [p U q]
E [ p U q ] ∃ [p U q]
AF p ∀◊
EF p ∃◊
AG p ∀□
EG p ∃□

Using spaces between U, AF, EF, AG, EG, AX, EX and a formula is recommended to avoid parse errors.

Precedence

The precedence of the operators is given in the following order, beginning with the operators with the most precedence to the ones with the least precedence. The operators that are on the same item have the same precedence.

  • Left associative: &, |

  • Left associative: ->

  • !, AX, EX, EF, AF, AG, EG, EU, AU

If you are not sure you can always use parentheses to explicit the order you want in your formula.