Skip to content

Commit

Permalink
Added optimizations of the algorithm, updated help file and version.
Browse files Browse the repository at this point in the history
  • Loading branch information
Mikulas Klokocka committed Apr 27, 2017
1 parent 82a16d7 commit 6b60569
Show file tree
Hide file tree
Showing 4 changed files with 124 additions and 528 deletions.
58 changes: 58 additions & 0 deletions formulae/liberouter.ltl
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
G ( (F p1) && (F ! p1) )
(G F p1) && (G F !p1)
G F ( !(p1 <-> (X p1)) || !(p2 <-> (X p2)) )
G F ( !(p1 <-> (X p1)) || !(p2 <-> (X p2)) || !(p3 <-> (X p3)) || !(p4 <-> (X p4)) )
G( ! ( p1 ))
G ( (p1 -> F (!p1)) && ((!p1) -> F p1) )
G ( p1 -> (F ( p1 && p2)))
G ( p1 -> F ( !p1 && p2 && p3 && p4 -> F p5))
G (p1 -> F !p2)
G (p1 -> F p2 )
G ( p1 -> F ( p2 -> F p3))
G ( p1 -> F ( p2 && p3 -> F p4))
G ((p1 -> F p2) && (p3 -> F p4) && (p5 -> F p6) && (p7 -> F p8))
G ( !p1 && !( p2) )
G (! ( p1 && p2 ) )
G ((p1)->(p2))
G ( (p1 -> (!p2)) && (p2 -> (!p1)))
G ((!p1) -> (p2 <-> !p3))
G ( ((p1 || p2 || p3) && !p4) -> p5)
G ((p1&&(p2)) -> (p3 || !(p4 && p5)))
G ( ((!p1) && p2 && (!p3) && (!p4) && (!p5)) -> (F ((!p6) && (!p7) && (!p8) && (!p9) )))
G ( (p1 && p2 && (!p3) && (!p4) && (!p5)) -> (F (p6 && (!p7) && (!p8) && (!p9) )))
G (!p1 -> !(p2 && p3 && p4 && p5 && p6))
G (!p1 -> ((p2 && p3 && p4 && p5)-> (! p6 ) ))
G ((p1&&(p2)) -> (p3 || p4 || !(p5 && p6)))
G (((!p1)&&(p2||p3||p4||p5))-> ((!p6) <-> p7))
G ((p1&&(p2)) -> (p3 || p4 || p5 || !(p6 && p7)))
G ((p1&&(p2)) -> (p3 || p4 || p5 || p6 || !(p7 && p8)))
G( (p1) && p2 && !p3 && X p3 -> X ( p4 || X (!p2 || p4)))
G( ( (p1) && p2 && !p3 && ( X p3 )) -> ( X ( ( X !p2 ) || ( p3 U ( (!p3) U ( p3 U ( !p2 || p4 ) ))))))
G( ( (p1)) && p2 && !p3 && ( X p3 )) -> ( X ( ( X !p2 ) || ( p3 U ( (!p3) U ( p3 U ( !p2 || p4 ) )))))
G( ( (p1) ) -> ( p2 U ( (!p2) U ( (!p3) || p4 ) ) ))
G( ( p1 ) -> ( p2 U ( (!p2) U ( (!p3) || p4 ) ) ))
G( ( p1 ) -> ( p2 U ( (!p2) U ( (p3) || p4 ) ) ))
G ( ( !p1 && p2 ) -> ( X p3 ) )
G ( ( !p1 && p2 ) -> (X p3) )
G ((p1) -> X( (p1) || (p2) ) )
G ( ( !(p1 <-> (X p1)) || !(p2 <-> (X p2)) || !(p3 <-> (X p3)) || !(p4 <-> (X p4)) ) -> ( (X !p5) && X ( (!( !(p1 <-> (X p1)) || !(p2 <-> (X p2)) || !(p3 <-> (X p3)) || !(p4 <-> (X p4)) )) U p5 ) ) )
G ( ( !(p1 <->(X p1)) || !(p2 <-> (X p2)) || !(p3 <-> (X p3)) || !(p4 <-> (X p4)) ) -> ( (X !p5) && X ( (!( !(p1 <-> (X p1)) || !(p2 <-> (X p2)) || !(p3 <-> (X p3)) || !(p4 <-> (X p4)) )) U p5 ) ) )
G ( ( p1 && X p1 && !p2 && X p2 -> ( ( p3) -> X p4)))
G ( p1 -> X ((!p1) U p2) )
G ( ((!p1) && X p1) -> X ( ( p1 U p2) || ( G p1) ))
G (((!p1) && X p1) -> X ( p1 U (((!p2) && p1) && X (p2 && p1) ) ) )
G (((!p1) && X p1) -> X ( p1 U (((!p2) && p1) && X (p2 && p1 && (p1 U (((!p2) && p1) && X (p2 && p1) ) ) ) ) ) )
G ((p1 && X (!p1)) -> X ( (!p1) U (((!p2) && (!p1)) && X (p2 && (!p1) && ((!p1) U (((!p2) && (!p1)) && X (p2 && (!p1)) ) ) ) ) ) )
G ((p1 && X (!p1)) -> X ( (!p1) U (((!p2) && (!p1)) && X (p2 && (!p1) && ((!p1) U (((!p2) && (!p1)) && X (p2 && (!p1) && ((!p1) U (((!p2) && (!p1)) && X (p2 && (!p1))) ) ) ) ) ) ) ) )
G ( ((!p1) && X p1) -> X ( (!((!p1) && X p1)) U ((!p2) && X p2) ) )
G (!(p1) || X(!(p1) || X(!(p1) || X(!(p1) || X(!(p1) || X(!(p1) || X(!(p1) || X(!(p1) || X(!(p1) || X(!(p1) || X(!(p1) || X(!(p1)))))))))))))
G (((X p1) -> p1)->((p2<->X p2)))
G (((X p1) -> p1)->((p2->X p2)&&((!p2) -> (X !p2))))
((!p1) U G ( ! ( ( p2 && p3 ) || ( p2 && p4 ) || ( p2 && p5) || ( p3 && p4 ) || ( p3 && p5) || ( p4 && p5 ) ) ))
((!p1) U p2)
( p1 U p2) || G p1
p1 && X G (!p1)
X G (p1 -> ((G !p2) || ((!X p2) U p3 )))
X G ((p1 && !p2)->(((!p2) U p3)||(G (!p2))))
X G ((p1 && p2)->((p2 U p3)||(G p2)))
(X p1) && ( G ((!p1 && X p1)-> X X p1 ))
257 changes: 0 additions & 257 deletions formulae/rand_det.ltl
View file

This file was deleted.

Loading

0 comments on commit 6b60569

Please sign in to comment.