Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
PMC-SOG
experiments
hybrid
Commits
afc73a79
Commit
afc73a79
authored
Apr 26, 2020
by
Jaime Arias
Browse files
Add new formulas with state space >= 1000 states
parent
cb503c9b
Changes
1000
Hide whitespace changes
Inline
Side-by-side
Too many changes to show.
To preserve performance only
1000 of 1000+
files are displayed.
Plain diff
Email patch
formulas/philo/philo10/philo10-1.ltl
View file @
afc73a79
((Eat_5==1) && ((Catch1_10==1) <-> <>(Catch1_3==1))) <-> []((Catch1_1==1) || (Catch1_5==1) || []<>(Catch2_9==1))
((Eat_5==1) && ((Catch1_10==1) <->
(
<>(Catch1_3==1)))
)
<->
(
[]((Catch1_1==1) || (Catch1_5==1) ||
(
[]
(
<>(Catch2_9==1))
)))
\ No newline at end of file
formulas/philo/philo10/philo10-1.ltl.reduced
View file @
afc73a79
(("Eat_5") && (("Catch1_10") <-> <>("Catch1_3"))) <-> [](("Catch1_1") || ("Catch1_5") || []<>("Catch2_9"))
(("Eat_5") && (("Catch1_10") <->
(
<>("Catch1_3")))
)
<->
(
[](("Catch1_1") || ("Catch1_5") ||
(
[]
(
<>("Catch2_9"))
)))
\ No newline at end of file
formulas/philo/philo10/philo10-10.ltl
View file @
afc73a79
[](
Think_6==1) <-> [](<>(Catch2_6
==1) && (
(
(Catch1_
6
==1) -> ((Catch2_
1
==1)
||
(Catch2_
2
==1)
)) || [](Catch2_1
==1)))
[](
(((Catch1_8==1) || (Fork_4
==1)
)
&& (
[](<>
(Catch1_
8
==1)
)))
-> ((Catch2_
3
==1)
<-> (
(Catch2_
6
==1)
<-> (Fork_4
==1)))
)
\ No newline at end of file
formulas/philo/philo10/philo10-10.ltl.reduced
View file @
afc73a79
[](
"Think_6") <-> [](<>("Catch2_6"
) && (
(
("Catch1_
6
") -> (("Catch2_
1
")
||
("Catch2_
2
")
)) || []("Catch2_1"
)))
[](
((("Catch1_8") || ("Fork_4")
) && (
[](<>
("Catch1_
8
")
)))
-> (("Catch2_
3
")
<-> (
("Catch2_
6
")
<-> ("Fork_4")
)))
\ No newline at end of file
formulas/philo/philo10/philo10-100.ltl
View file @
afc73a79
[]((Catch2_9==1) -> (<>!(Thin
k_
8
==1)
-> !(<>
(Catch1_
10
==1)
-> <>(Think_5==1
))))
!(<>((<>(!([](<>(For
k_
6
==1)
)))) && (!([](!
(Catch1_
4
==1)
)
))))
\ No newline at end of file
formulas/philo/philo10/philo10-100.ltl.reduced
View file @
afc73a79
[](("Catch2_9") -> (<>!("Thin
k_
8
")
-> !(<>("Catch1_10") -> <>("Think_5"
))))
!(<>((<>(!([](<>("For
k_
6
")
)))) && (!([](!("Catch1_4"))
))))
\ No newline at end of file
formulas/philo/philo10/philo10-101.ltl
View file @
afc73a79
[]((!(Fork_10==1) ||
(Think_
2
==1))
-> ((Fork_3==1) <-> (<>(Eat_10==1) || [])))
(<>([]
(Think_
3
==1))
) <-> ((Catch1_3==1) || (<>([](Think_3
==1))))
\ No newline at end of file
formulas/philo/philo10/philo10-101.ltl.reduced
View file @
afc73a79
[]((!("Fork_10") ||
("Think_
2
"))
-> (("Fork_3"
) <-> (
<>
("
E
at
_10
") ||
[])))
(<>([]
("Think_
3
"))) <-> (("
C
at
ch1_3
") ||
(<>([]("Think_3
"))))
\ No newline at end of file
formulas/philo/philo10/philo10-102.ltl
View file @
afc73a79
((Eat_9
==1)
&&
(Fork_
3
==1)
) || <>
((Catch
1_7
==1) && (
((Catch2_1==1) || []<>[](Catch1_10==1)) -> (Catch2_1==1
)))
[](([](Catch1_6
==1)
)
-> (
(Fork_
5
==1)
<->
((Catch
2_5
==1) && (
[](!(Eat_10==1)))
)))
\ No newline at end of file
formulas/philo/philo10/philo10-102.ltl.reduced
View file @
afc73a79
(
("
E
at
_9") &&
("Fork_
3
")
) || <>
(("Catch
1_7
") && (
(("Catch2_1") || []<>
[]("
C
at
ch1
_10"))
-> ("Catch2_1"
)))
[](([]
("
C
at
ch1_6")) -> (
("Fork_
5
")
<->
(("Catch
2_5
") && ([]
(!
("
E
at_10"))
)
)))
\ No newline at end of file
formulas/philo/philo10/philo10-103.ltl
View file @
afc73a79
(Catch1_2==1) || (<>((Catch1
_1
0
==1) && (Think_8==1)
)
-> (
Catch1_7==1)) || (<>(Catch1_5==1) && <>[](Think_2==1
))
!([]((Fork
_1==1) &&
(!([](
(Think_8==1) -> (
<>((Eat_1==1) <-> ([](Eat_2==1)))))))
))
\ No newline at end of file
formulas/philo/philo10/philo10-103.ltl.reduced
View file @
afc73a79
("Catch1_2") || (<>(("Catch1
_1
0
") && ("Think_8")
)
->
("Catch1_7")) ||
(<>("
C
at
ch1_5") && <>[]("Think_2"
))
!([](("Fork
_1") &&
(!([](
("Think_8") -> (<>(
(
"
E
at
_1") <-> ([]("Eat_2")))))))
))
\ No newline at end of file
formulas/philo/philo10/philo10-104.ltl
View file @
afc73a79
!(Eat_4==1
) || (((Eat_
2
==1)
|| (For
k_8==1))
<
->
!(!((Fork_6
==1)
||
(Think_3==1))
|| <>(Catch1_1==1
)))
[](((Catch1_3==1) -> ([](Think_1==1))
) || (((Eat_
3
==1)
&& (Thin
k_8==1)) ->
(<>((!(Catch1_1
==1)
)
&&
(Think_3==1)))))
\ No newline at end of file
formulas/philo/philo10/philo10-104.ltl.reduced
View file @
afc73a79
!
("
E
at
_4"
) || ((("Eat_
2
")
||
("
For
k_8"))
<
->
!
(!(
(
"
Fork_6") || ("Think_3")) || <>("Catch1_1"
)))
[]((
("
C
at
ch1_3") -> ([]("Think_1"))
) || ((("Eat_
3
")
&&
("
Thin
k_8")) ->
(<>(
(!("
Catch1_1")) && ("Think_3"))
)))
\ No newline at end of file
formulas/philo/philo10/philo10-105.ltl
View file @
afc73a79
!(((Fork_3==1) || [](Think_7==1) || ((
(Eat_
3
==1)
<
-> (Think_
5
==1)
)
&& [](
E
at
_8
==1)))
-> (Eat_4==1
))
[](<>(([](!
(Eat_
5
==1)
))
->
(!([](
(Think_
3
==1) &&
(<>(
[](
C
at
ch2_3
==1)))
)))
))
\ No newline at end of file
formulas/philo/philo10/philo10-105.ltl.reduced
View file @
afc73a79
!((("Fork_3") || []("Think_7") || ((
("Eat_
3
")
<
-> ("Think_
5
")
)
&& []("
E
at
_8"))) -> ("Eat_4"
))
[](<>(([](!
("Eat_
5
")
))
->
(!([](
("Think_
3
") &&
(<>(
[]("
C
at
ch2_3"))))))
))
\ No newline at end of file
formulas/philo/philo10/philo10-106.ltl
View file @
afc73a79
<>
(((Eat_
10
==1) -> (Eat_
1
==1)
) && <>(Fork_8==1)) -> !
((Catch1_
8
==1) -> (
Catch2_1
==1))
[]
(((Eat_
8
==1) ->
(
(Eat_
2
==1)
-> (Catch2_9==1))) || (([](<>
((Catch1_
2
==1)
<
-> (
Think_2==1)))) -> (!(Fork_8
==1))
))
\ No newline at end of file
formulas/philo/philo10/philo10-106.ltl.reduced
View file @
afc73a79
<>
((("Eat_
10
") -> ("Eat_
1
")
) && <>("Fork_8")) -> !
(("Catch1_
8
") -> ("
Catch2_1
"))
[]
((("Eat_
8
") ->
(
("Eat_
2
")
-> ("Catch2_9"))) || (([](<>
(("Catch1_
2
")
<
-> ("
Think_2")))) -> (!("Fork_8
"))
))
\ No newline at end of file
formulas/philo/philo10/philo10-107.ltl
View file @
afc73a79
!
((Eat_2==1)
|| [](Think_9==1) ||
[](
(
Catch1_
9
==1)
|| !(Eat_9
==1)))
<>([](([]
((Eat_2==1)
&& ((<>(!(Catch1_8==1))) <-> (<>(
[](Catch1_
8
==1)
))))) -> ([](Think_8
==1)))
)
\ No newline at end of file
formulas/philo/philo10/philo10-107.ltl.reduced
View file @
afc73a79
!
(("Eat_2")
|| []("Think_9") ||
[](
(
"Catch1_
9
")
|| !("Eat_9"
)))
<>([](([]
(("Eat_2")
&& ((<>(!("Catch1_8"))) <-> (<>(
[]("Catch1_
8
")
))))) -> ([]("Think_8")
)))
\ No newline at end of file
Prev
1
2
3
4
5
…
50
Next
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment