Skip to content
Snippets Groups Projects
Commit 965fea88 authored by Jaime Arias's avatar Jaime Arias
Browse files

Merge

parents 3d0bb53a 4031b231
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 17 additions and 5892 deletions
.gitignore
+ 0
− 4
View file @ 965fea88
......@@ -69,10 +69,6 @@ obj/
### Code ###
.vscode/*
!.vscode/settings.json
!.vscode/tasks.json
!.vscode/launch.json
!.vscode/extensions.json
### Eclipse ###
.metadata
......
.gitmodules
+ 3
− 1
View file @ 965fea88
......@@ -5,4 +5,6 @@
path = third-party/sylvan
url = https://depot.lipn.univ-paris13.fr/PMC-SOG/sylvan.git
branch = Sylvan-SOG
\ No newline at end of file
[submodule "third-party/spot"]
path = third-party/spot
url = https://gitlab.lrde.epita.fr/spot/spot.git
.gitmodules.save deleted 100644 → 0
+ 0
− 4
View file @ 3d0bb53a
[submodule "libraries/parser"]
path = libraries/parser
url = https://depot.lipn.univ-paris13.fr/PMC-SOG/pn-parser/tree/mc-sog-parser
URL non trouvée pour le chemin de sous-mod
CMakeLists.txt
+ 14
− 3
View file @ 965fea88
......@@ -2,7 +2,7 @@
cmake_minimum_required(VERSION 3.5 FATAL_ERROR)
# project name and language
project(hybrid-sog C CXX)
project(pmc-sog C CXX)
# compiler flags
if(CMAKE_COMPILER_IS_GNUCC)
......@@ -15,14 +15,25 @@ message(STATUS "Building Petri Net parser ...")
include_directories("${PARSER_DIR}/src")
add_subdirectory(${PARSER_DIR})
# add sylvan
message(STATUS "Building Sylvan ...")
set(SYLVAN_DIR "${CMAKE_SOURCE_DIR}/third-party/sylvan")
include_directories(${SYLVAN_DIR})
add_subdirectory(${SYLVAN_DIR})
# add spot
include(ExternalProject)
message(STATUS "Building Spot ...")
set(SPOT_SOURCE_DIR "${CMAKE_SOURCE_DIR}/third-party/spot")
set(SPOT_DIR "${CMAKE_BINARY_DIR}/third-party/spot")
ExternalProject_Add(SpotLibrary
PREFIX ${SPOT_DIR}
SOURCE_DIR ${SPOT_SOURCE_DIR}
CONFIGURE_COMMAND autoreconf -if ${SPOT_SOURCE_DIR} && ${SPOT_SOURCE_DIR}/configure --disable-python --prefix=<INSTALL_DIR>
BUILD_COMMAND make -j
)
include_directories("${SPOT_DIR}/include")
# add source folder
include_directories(src)
add_subdirectory(src)
......
Examples/philo/.svn/all-wcprops deleted 100644 → 0
+ 0
− 449
View file @ 3d0bb53a
K 25
svn:wc:ra_dav:version-url
V 56
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo
END
philo100.net
K 25
svn:wc:ra_dav:version-url
V 69
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo100.net
END
philo2.net.smv
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo2.net.smv
END
philo3.net.smv
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo3.net.smv
END
philo4.net.smv
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo4.net.smv
END
philo5.net.smv
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo5.net.smv
END
philo6.net.smv
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo6.net.smv
END
philo7.net.smv
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo7.net.smv
END
philo8.net.smv
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo8.net.smv
END
philo20.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo20.net.ltl
END
philo9.net.smv
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo9.net.smv
END
philo22.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo22.net.ltl
END
philo10.net.ltl.smv
K 25
svn:wc:ra_dav:version-url
V 76
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo10.net.ltl.smv
END
philo24.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo24.net.ltl
END
philo26.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo26.net.ltl
END
philo28.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo28.net.ltl
END
philo30.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo30.net.smv
END
philo32.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo32.net.smv
END
philo.sed.org
K 25
svn:wc:ra_dav:version-url
V 70
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo.sed.org
END
philo2.net.ltl
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo2.net.ltl
END
philo3.net.ltl
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo3.net.ltl
END
philo4.net.ltl
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo4.net.ltl
END
philo5.net.ltl
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo5.net.ltl
END
philo6.net.ltl
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo6.net.ltl
END
philo7.net.ltl
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo7.net.ltl
END
philo8.net.ltl
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo8.net.ltl
END
philo9.net.ltl
K 25
svn:wc:ra_dav:version-url
V 71
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo9.net.ltl
END
philo100.net.smv
K 25
svn:wc:ra_dav:version-url
V 73
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo100.net.smv
END
philo30.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo30.net.ltl
END
philo32.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo32.net.ltl
END
formula.ltl
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/formula.ltl
END
philo10.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo10.net
END
philo12.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo12.net
END
philo14.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo14.net
END
philo50.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo50.net
END
philo16.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo16.net
END
mctest.sh
K 25
svn:wc:ra_dav:version-url
V 66
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/mctest.sh
END
philo18.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo18.net
END
philo100.net.ltl
K 25
svn:wc:ra_dav:version-url
V 73
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo100.net.ltl
END
philo20.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo20.net
END
toto.txt
K 25
svn:wc:ra_dav:version-url
V 65
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/toto.txt
END
formula.ltl.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/formula.ltl.smv
END
philo22.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo22.net
END
philo10.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo10.net.smv
END
philo24.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo24.net
END
philo12.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo12.net.smv
END
philo26.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo26.net
END
philo14.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo14.net.smv
END
philo50.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo50.net.smv
END
philo28.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo28.net
END
philo16.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo16.net.smv
END
philo18.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo18.net.smv
END
philo2.net
K 25
svn:wc:ra_dav:version-url
V 67
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo2.net
END
philo3.net
K 25
svn:wc:ra_dav:version-url
V 67
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo3.net
END
philo4.net
K 25
svn:wc:ra_dav:version-url
V 67
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo4.net
END
philo.sed
K 25
svn:wc:ra_dav:version-url
V 66
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo.sed
END
philo5.net
K 25
svn:wc:ra_dav:version-url
V 67
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo5.net
END
philo6.net
K 25
svn:wc:ra_dav:version-url
V 67
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo6.net
END
philo7.net
K 25
svn:wc:ra_dav:version-url
V 67
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo7.net
END
philo8.net
K 25
svn:wc:ra_dav:version-url
V 67
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo8.net
END
philo9.net
K 25
svn:wc:ra_dav:version-url
V 67
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo9.net
END
philo10.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo10.net.ltl
END
philo12.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo12.net.ltl
END
philo14.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo14.net.ltl
END
philo50.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo50.net.ltl
END
philo16.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo16.net.ltl
END
philo30.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo30.net
END
philo18.net.ltl
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo18.net.ltl
END
philo32.net
K 25
svn:wc:ra_dav:version-url
V 68
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo32.net
END
philo20.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo20.net.smv
END
philo22.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo22.net.smv
END
philo24.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo24.net.smv
END
philo.ap
K 25
svn:wc:ra_dav:version-url
V 65
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo.ap
END
philo26.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo26.net.smv
END
philo28.net.smv
K 25
svn:wc:ra_dav:version-url
V 72
/svn/research/dp/!svn/ver/1/checksog-state/samples/philo/philo28.net.smv
END
Examples/philo/.svn/entries deleted 100644 → 0
+ 0
− 918
View file @ 3d0bb53a
8
dir
5
https://srcdev.lip6.fr/svn/research/dp/checksog-state/samples/philo
https://srcdev.lip6.fr/svn/research/dp
2008-06-12T11:03:53.142753Z
1
dp
svn:special svn:externals svn:needs-lock
a394a755-3a4f-4fec-9ee5-bbc2ad5c66d4
philo100.net
file
2008-06-16T13:32:03.000000Z
10c9eb8808d8fc9838ffda69708dfad2
2008-06-12T11:03:53.142753Z
1
dp
philo2.net.smv
file
2008-06-16T13:32:03.000000Z
d830cac5564765f52885b5daaeba0c6f
2008-06-12T11:03:53.142753Z
1
dp
philo3.net.smv
file
2008-06-16T13:32:03.000000Z
f6a4f7af6e9316908e0b0f23548a8104
2008-06-12T11:03:53.142753Z
1
dp
philo4.net.smv
file
2008-06-16T13:32:03.000000Z
339ae058ca903a19d0b7008b0d8c86e2
2008-06-12T11:03:53.142753Z
1
dp
philo5.net.smv
file
2008-06-16T13:32:03.000000Z
b98a631fd096f7a7bf3f4066d0cd0991
2008-06-12T11:03:53.142753Z
1
dp
philo6.net.smv
file
2008-06-16T13:32:03.000000Z
cbb1140d15aec9284b2b11889d2a1d6d
2008-06-12T11:03:53.142753Z
1
dp
philo7.net.smv
file
2008-06-16T13:32:03.000000Z
d9d2ca8006d771b7abed30686dcf57d6
2008-06-12T11:03:53.142753Z
1
dp
philo8.net.smv
file
2008-06-16T13:32:03.000000Z
1a00677389627e71aacad6d9d16e41bd
2008-06-12T11:03:53.142753Z
1
dp
philo20.net.ltl
file
2008-06-16T13:32:03.000000Z
2472b291ed23cfe79d06e1dfc08572c9
2008-06-12T11:03:53.142753Z
1
dp
philo9.net.smv
file
2008-06-16T13:32:04.000000Z
a0ce1c2550e0fa189c531b20ebf5f177
2008-06-12T11:03:53.142753Z
1
dp
philo22.net.ltl
file
2008-06-16T13:32:04.000000Z
2472b291ed23cfe79d06e1dfc08572c9
2008-06-12T11:03:53.142753Z
1
dp
philo10.net.ltl.smv
file
2008-06-16T13:32:04.000000Z
610e1b7fcf704822ae7dc3863d239cfd
2008-06-12T11:03:53.142753Z
1
dp
philo24.net.ltl
file
2008-06-16T13:32:04.000000Z
2472b291ed23cfe79d06e1dfc08572c9
2008-06-12T11:03:53.142753Z
1
dp
philo26.net.ltl
file
2008-06-16T13:32:04.000000Z
aa01acce080ce9e924c0787eced3b4df
2008-06-12T11:03:53.142753Z
1
dp
philo28.net.ltl
file
2008-06-16T13:32:04.000000Z
bdecfb2bd63b9cb31fd46a07a0b6bb73
2008-06-12T11:03:53.142753Z
1
dp
philo30.net.smv
file
2008-06-16T13:32:04.000000Z
bf64d759c8bd0073e18e709c0858727d
2008-06-12T11:03:53.142753Z
1
dp
philo32.net.smv
file
2008-06-16T13:32:04.000000Z
399943875c76fe21c1ee110a83b72d23
2008-06-12T11:03:53.142753Z
1
dp
philo.sed.org
file
2008-06-16T13:32:04.000000Z
babdd436d7edbe2bf916bf0f930da724
2008-06-12T11:03:53.142753Z
1
dp
philo2.net.ltl
file
2008-06-16T13:32:04.000000Z
cf732275d6549380b331df1fa4709356
2008-06-12T11:03:53.142753Z
1
dp
philo3.net.ltl
file
2008-06-16T13:32:04.000000Z
4729b2c6ebee1c578431f9ea42bcd8b1
2008-06-12T11:03:53.142753Z
1
dp
philo4.net.ltl
file
2008-06-16T13:32:04.000000Z
f484666840b501844529247d95a8a0aa
2008-06-12T11:03:53.142753Z
1
dp
philo5.net.ltl
file
2008-06-16T13:32:04.000000Z
ad26df12a3424f6964c58847734cdfda
2008-06-12T11:03:53.142753Z
1
dp
philo6.net.ltl
file
2008-06-16T13:32:04.000000Z
14ae886bd1fcc7cd5dda00d91c160307
2008-06-12T11:03:53.142753Z
1
dp
philo7.net.ltl
file
2008-06-16T13:32:05.000000Z
c0d89c139677af0a4d8789672be1d5f8
2008-06-12T11:03:53.142753Z
1
dp
philo8.net.ltl
file
2008-06-16T13:32:05.000000Z
9ce7b5aeb2467d12198f154b9b67a630
2008-06-12T11:03:53.142753Z
1
dp
philo9.net.ltl
file
2008-06-16T13:32:05.000000Z
6e5aaff7e92b684474375c15e3d6ddbd
2008-06-12T11:03:53.142753Z
1
dp
philo100.net.smv
file
2008-06-16T13:32:06.000000Z
0fe0644c25c73acbe08b195529a0a2ad
2008-06-12T11:03:53.142753Z
1
dp
philo30.net.ltl
file
2008-06-16T13:32:06.000000Z
f209c2866591b9e88030ecdcf871a8e8
2008-06-12T11:03:53.142753Z
1
dp
philo32.net.ltl
file
2008-06-16T13:32:06.000000Z
f209c2866591b9e88030ecdcf871a8e8
2008-06-12T11:03:53.142753Z
1
dp
formula.ltl
file
2008-06-16T13:32:06.000000Z
d119c64748b51208b0098480249dbaa1
2008-06-12T11:03:53.142753Z
1
dp
philo10.net
file
2008-06-16T13:32:06.000000Z
e01766d652bd6117fc956a3d5f12c40d
2008-06-12T11:03:53.142753Z
1
dp
philo12.net
file
2008-06-16T13:32:06.000000Z
a0908d4f435c20c1542a47852b50446f
2008-06-12T11:03:53.142753Z
1
dp
philo14.net
file
2008-06-16T13:32:06.000000Z
72bfe3ffc472289156508275fc585af3
2008-06-12T11:03:53.142753Z
1
dp
philo50.net
file
2008-06-16T13:32:06.000000Z
f6d39b7b3b77b7236481bb9cac4d8a82
2008-06-12T11:03:53.142753Z
1
dp
philo16.net
file
2008-06-16T13:32:06.000000Z
f855800df5e3b2e9ec257037df16e1eb
2008-06-12T11:03:53.142753Z
1
dp
mctest.sh
file
2008-06-16T13:32:06.000000Z
4633ac629e1c3709f5480166f7874b48
2008-06-12T11:03:53.142753Z
1
dp
has-props
philo18.net
file
2008-06-16T13:32:06.000000Z
1e717752ab90e7f1e284374ed359664a
2008-06-12T11:03:53.142753Z
1
dp
philo100.net.ltl
file
2008-06-16T13:32:06.000000Z
14d2e622f263aebafab4e5a2c92bb81a
2008-06-12T11:03:53.142753Z
1
dp
philo20.net
file
2008-06-16T13:32:06.000000Z
3b2ccc874cc00cd93878f0f22756b534
2008-06-12T11:03:53.142753Z
1
dp
toto.txt
file
2008-06-16T13:32:06.000000Z
a587283765a89c78ea72266441ab632a
2008-06-12T11:03:53.142753Z
1
dp
has-props
formula.ltl.smv
file
2008-06-16T13:32:06.000000Z
ed0c835feb76d301c4651ff35e01cdda
2008-06-12T11:03:53.142753Z
1
dp
philo22.net
file
2008-06-16T13:32:06.000000Z
281395875d191a651bfab6e28f9b2d15
2008-06-12T11:03:53.142753Z
1
dp
philo10.net.smv
file
2008-06-16T13:32:06.000000Z
808fcff7f5172b3d6ffe0ed1f05b6834
2008-06-12T11:03:53.142753Z
1
dp
philo24.net
file
2008-06-16T13:32:07.000000Z
e385e9d4e002a1b5cc7d497539256594
2008-06-12T11:03:53.142753Z
1
dp
philo12.net.smv
file
2008-06-16T13:32:07.000000Z
0ad16159c4ad10c0e02740861325a3c9
2008-06-12T11:03:53.142753Z
1
dp
philo26.net
file
2008-06-16T13:32:07.000000Z
fa06c0191f7fd420057133042ac86df2
2008-06-12T11:03:53.142753Z
1
dp
philo14.net.smv
file
2008-06-16T13:32:07.000000Z
daf3e94ade98d670fb3b683a33e01930
2008-06-12T11:03:53.142753Z
1
dp
philo50.net.smv
file
2008-06-16T13:32:07.000000Z
8566eb073ece7894967d1bef109b4126
2008-06-12T11:03:53.142753Z
1
dp
philo28.net
file
2008-06-16T13:32:07.000000Z
fc1b6d74bfa49cf616530d6dc646038b
2008-06-12T11:03:53.142753Z
1
dp
philo16.net.smv
file
2008-06-16T13:32:07.000000Z
6afe50bf2f0fd4c553a49009ca2d9096
2008-06-12T11:03:53.142753Z
1
dp
philo18.net.smv
file
2008-06-16T13:32:07.000000Z
04f9748bf21b26e49792ea00ccba5399
2008-06-12T11:03:53.142753Z
1
dp
philo2.net
file
2008-06-16T13:32:08.000000Z
ac2f6c765563bb5e8e7bd1d7d6848fa3
2008-06-12T11:03:53.142753Z
1
dp
philo3.net
file
2008-06-16T13:32:08.000000Z
be4b461ce2c66e054a093ca4a6151016
2008-06-12T11:03:53.142753Z
1
dp
philo4.net
file
2008-06-16T13:32:08.000000Z
8bf86a37c907cdefacc0d551b574fb99
2008-06-12T11:03:53.142753Z
1
dp
philo.sed
file
2008-06-16T13:32:08.000000Z
737c8f8c19dd36cce97fc39c6d311f7c
2008-06-12T11:03:53.142753Z
1
dp
philo5.net
file
2008-06-16T13:32:08.000000Z
912f643ee02c5d53033c334ab75541b0
2008-06-12T11:03:53.142753Z
1
dp
philo6.net
file
2008-06-16T13:32:08.000000Z
c659273ff443b4f9d47ca2f27f094bcd
2008-06-12T11:03:53.142753Z
1
dp
philo7.net
file
2008-06-16T13:32:08.000000Z
d7aaa23b690e41092d30f4487ee2ed64
2008-06-12T11:03:53.142753Z
1
dp
philo8.net
file
2008-06-16T13:32:08.000000Z
e676140755ea611b4e4dc09f65b8061f
2008-06-12T11:03:53.142753Z
1
dp
philo9.net
file
2008-06-16T13:32:08.000000Z
d84d0bcff3a6e07f86e26ba18f15613c
2008-06-12T11:03:53.142753Z
1
dp
philo10.net.ltl
file
2008-06-16T13:32:08.000000Z
be2a6cc9275cc10c7ac06c7ed0be2900
2008-06-12T11:03:53.142753Z
1
dp
philo12.net.ltl
file
2008-06-16T13:32:08.000000Z
b2ca99cdff0df1894a79d9ece4f99285
2008-06-12T11:03:53.142753Z
1
dp
philo50.net.ltl
file
2008-06-16T13:32:08.000000Z
c9c946d276615a6aa69faf256dcf8345
2008-06-12T11:03:53.142753Z
1
dp
philo14.net.ltl
file
2008-06-16T13:32:08.000000Z
6637b2e8b7607a49d72246fd18e78696
2008-06-12T11:03:53.142753Z
1
dp
philo16.net.ltl
file
2008-06-16T13:32:08.000000Z
01bb3e2654e5afb5ea64e4716c890aeb
2008-06-12T11:03:53.142753Z
1
dp
philo30.net
file
2008-06-16T13:32:08.000000Z
42be39419516cea8bf02068b64b444c2
2008-06-12T11:03:53.142753Z
1
dp
philo18.net.ltl
file
2008-06-16T13:32:08.000000Z
f644272b2b12053ab0313fd1078e6488
2008-06-12T11:03:53.142753Z
1
dp
philo32.net
file
2008-06-16T13:32:08.000000Z
77249ad7a11f76bf14f18f9b72391b4e
2008-06-12T11:03:53.142753Z
1
dp
philo20.net.smv
file
2008-06-16T13:32:09.000000Z
c7b4927128376e517e82ef0227cfb91c
2008-06-12T11:03:53.142753Z
1
dp
philo22.net.smv
file
2008-06-16T13:32:09.000000Z
0fa2fa04c3da359edf2adfea7cc94211
2008-06-12T11:03:53.142753Z
1
dp
philo24.net.smv
file
2008-06-16T13:32:09.000000Z
b3b287d88928b016701fe3f115fd405a
2008-06-12T11:03:53.142753Z
1
dp
philo.ap
file
2008-06-16T13:32:09.000000Z
d9395129d019127410b6bde81f34c647
2008-06-12T11:03:53.142753Z
1
dp
philo26.net.smv
file
2008-06-16T13:32:09.000000Z
b8110f9d7b32ca4e48229d22f56e4982
2008-06-12T11:03:53.142753Z
1
dp
philo28.net.smv
file
2008-06-16T13:32:09.000000Z
6fe5b141e2af1bf271ea0f9a6ff6fb55
2008-06-12T11:03:53.142753Z
1
dp
Examples/philo/.svn/format deleted 100644 → 0
+ 0
− 1
View file @ 3d0bb53a
8
Examples/philo/.svn/prop-base/mctest.sh.svn-base deleted 100644 → 0
+ 0
− 9
View file @ 3d0bb53a
K 13
svn:eol-style
V 6
native
K 14
svn:executable
V 1
*
END
Examples/philo/.svn/prop-base/toto.txt.svn-base deleted 100644 → 0
+ 0
− 5
View file @ 3d0bb53a
K 13
svn:eol-style
V 6
native
END
Examples/philo/.svn/text-base/formula.ltl.smv.svn-base deleted 100644 → 0
+ 0
− 100
View file @ 3d0bb53a
LTLSPEC !(G(!(Fork1>=1) & !(WaitRight0>=1)) & !(HasRight1>=1))
LTLSPEC !(((Idle1>=1) & ((HasRight1>=1) U !(HasLeft1>=1))) | (HasRight1>=1) | (!(Idle1>=1) & (!(HasRight1>=1) V (HasLeft1>=1))))
LTLSPEC !(((F!(IsEating0>=1) & (HasLeft1>=1)) | (!(HasLeft1>=1) & G(IsEating0>=1))) U (Idle1>=1))
LTLSPEC !((!(WaitRight0>=1) V (Idle1>=1)) V F!(IsEating1>=1))
LTLSPEC !((G!(Idle1>=1) & F((!(WaitLeft1>=1) & (HasRight0>=1)) | (!(HasRight0>=1) & (WaitLeft1>=1)))) | (F(Idle1>=1) & G((!(HasRight0>=1) | (WaitLeft1>=1)) & (!(WaitLeft1>=1) | (HasRight0>=1)))))
LTLSPEC !(((IsEating1>=1) & (((!(Fork1>=1) U (HasLeft0>=1)) & (WaitLeft0>=1)) | (((Fork1>=1) V !(HasLeft0>=1)) & !(WaitLeft0>=1)))) | (!(IsEating1>=1) & (((Fork1>=1) V !(HasLeft0>=1)) | !(WaitLeft0>=1)) & ((!(Fork1>=1) U (HasLeft0>=1)) | (WaitLeft0>=1))))
LTLSPEC !(((G!(WaitLeft0>=1) | !(Fork1>=1)) & ((Fork1>=1) | F(WaitLeft0>=1)) & (WaitRight1>=1)) | (((G!(WaitLeft0>=1) & !(Fork1>=1)) | ((Fork1>=1) & F(WaitLeft0>=1))) & !(WaitRight1>=1)))
LTLSPEC !(F((((G(IsEating1>=1) & G!(WaitRight0>=1)) | (F!(IsEating1>=1) & F(WaitRight0>=1))) & (HasLeft1>=1)) | (!(HasLeft1>=1) & (G(IsEating1>=1) | G!(WaitRight0>=1)) & (F!(IsEating1>=1) | F(WaitRight0>=1)))))
LTLSPEC !((!(IsEating0>=1) & (((Fork1>=1) & (HasRight0>=1) & (HasRight1>=1)) | (!(HasRight1>=1) & (!(HasRight0>=1) | !(Fork1>=1))))) | ((IsEating0>=1) & (!(HasRight0>=1) | !(HasRight1>=1) | !(Fork1>=1)) & (((Fork1>=1) & (HasRight0>=1)) | (HasRight1>=1))))
LTLSPEC !(F(HasRight0>=1) & (F(WaitLeft0>=1) | F(HasLeft1>=1)))
LTLSPEC !(((Idle0>=1) & G!(HasLeft0>=1)) | (!(Fork0>=1) & !(Idle0>=1)) | ((Fork0>=1) & (Idle0>=1)))
LTLSPEC !(((F!(Idle0>=1) V (!(IsEating0>=1) | !(WaitRight0>=1))) & (WaitRight0>=1)) | ((G(Idle0>=1) U ((WaitRight0>=1) & (IsEating0>=1))) & !(WaitRight0>=1)))
LTLSPEC !(((!(HasRight1>=1) & !(WaitLeft0>=1)) | ((HasRight1>=1) & (WaitLeft0>=1))) V (F(WaitLeft0>=1) | (IsEating0>=1)))
LTLSPEC !((F(!(Idle0>=1) | (WaitRight0>=1)) & (!(Fork1>=1) | (WaitLeft1>=1))) | ((Fork1>=1) & G((Idle0>=1) & !(WaitRight0>=1)) & !(WaitLeft1>=1)))
LTLSPEC !(G((!(IsEating1>=1) & !(Fork0>=1) & (WaitLeft0>=1)) | (!(WaitLeft0>=1) & ((Fork0>=1) | (IsEating1>=1)))))
LTLSPEC !((F(HasRight0>=1) & G!(Idle1>=1)) | (G!(HasRight0>=1) & F(Idle1>=1)))
LTLSPEC !(G(Idle1>=1) & (F!(HasRight0>=1) | !(Idle1>=1)))
LTLSPEC !(((WaitRight1>=1) | (HasLeft1>=1)) & ((F(IsEating0>=1) & (IsEating1>=1)) | (G!(IsEating0>=1) & !(IsEating1>=1))))
LTLSPEC !(F(WaitRight1>=1) U ((!(WaitLeft1>=1) & (((Idle0>=1) & !(HasLeft1>=1)) | (!(Idle0>=1) & (HasLeft1>=1)))) | ((!(Idle0>=1) | (HasLeft1>=1)) & (WaitLeft1>=1) & ((Idle0>=1) | !(HasLeft1>=1)))))
LTLSPEC !(((Idle0>=1) & (!(HasRight1>=1) | (G!(WaitLeft0>=1) U !(Idle0>=1))) & ((F(WaitLeft0>=1) V (Idle0>=1)) | (HasRight1>=1))) | (!(Idle0>=1) & ((!(HasRight1>=1) & (G!(WaitLeft0>=1) U !(Idle0>=1))) | ((F(WaitLeft0>=1) V (Idle0>=1)) & (HasRight1>=1)))))
LTLSPEC !((((WaitLeft0>=1) U (Fork1>=1)) & G(HasRight0>=1)) | (F!(HasRight0>=1) & (!(WaitLeft0>=1) V !(Fork1>=1))))
LTLSPEC !((!(Idle0>=1) & ((Fork0>=1) | (WaitRight1>=1)) & (!(Fork0>=1) | !(WaitRight1>=1))) | ((Idle0>=1) & (((Fork0>=1) & (WaitRight1>=1)) | (!(Fork0>=1) & !(WaitRight1>=1)))))
LTLSPEC !(F((Idle0>=1) | (!(HasLeft1>=1) & ((Idle1>=1) U (Fork0>=1))) | ((!(Idle1>=1) V !(Fork0>=1)) & (HasLeft1>=1))))
LTLSPEC !(((Fork1>=1) & !(HasLeft1>=1) & G!(WaitLeft0>=1)) | ((F(WaitLeft0>=1) | !(Fork1>=1)) & (HasLeft1>=1)))
LTLSPEC !((((G(IsEating0>=1) & F(HasLeft1>=1)) | (F!(IsEating0>=1) & G!(HasLeft1>=1))) & G(HasRight0>=1)) | (F!(HasRight0>=1) & (F!(IsEating0>=1) | G!(HasLeft1>=1)) & (G(IsEating0>=1) | F(HasLeft1>=1))))
LTLSPEC !((Idle1>=1) & ((Fork0>=1) | (F(HasRight1>=1) & !(Fork1>=1))))
LTLSPEC !((!(WaitLeft0>=1) | (HasRight0>=1)) U ((!(HasRight0>=1) & !(WaitRight1>=1)) | ((WaitRight1>=1) & (HasRight0>=1))))
LTLSPEC !((F G(HasLeft1>=1) & (G!(WaitRight1>=1) V !(WaitLeft1>=1))) | ((F(WaitRight1>=1) U (WaitLeft1>=1)) & G F!(HasLeft1>=1)))
LTLSPEC !(F!(WaitRight0>=1) | ((Fork0>=1) & F(WaitLeft0>=1)) | (G!(WaitLeft0>=1) & !(Fork0>=1)))
LTLSPEC !(!(IsEating0>=1) | ((Fork1>=1) & F!(Fork1>=1)))
LTLSPEC !(F(((Idle0>=1) & (!(Fork1>=1) U !(HasRight1>=1)) & (IsEating1>=1)) | (!(Idle0>=1) & (((Fork1>=1) V (HasRight1>=1)) | !(IsEating1>=1)))))
LTLSPEC !(F(((F!(WaitRight1>=1) | (HasRight1>=1)) & (!(HasRight1>=1) | G(WaitRight1>=1))) V !(IsEating1>=1)))
LTLSPEC !((!(HasRight0>=1) & G(WaitRight1>=1)) | (F!(WaitRight1>=1) & (HasRight0>=1)))
LTLSPEC !(F((!(HasLeft0>=1) & !(WaitRight0>=1)) | ((WaitRight0>=1) & (HasLeft0>=1))) U !(Idle0>=1))
LTLSPEC !((!(HasLeft0>=1) | (WaitLeft0>=1)) V (!(Fork0>=1) | (HasRight1>=1)))
LTLSPEC !((!(HasRight0>=1) & (((Fork1>=1) U (Fork0>=1)) V !(HasRight1>=1))) | (((!(Fork1>=1) V !(Fork0>=1)) U (HasRight1>=1)) & (HasRight0>=1)))
LTLSPEC !(((!(HasLeft1>=1) V (((HasRight1>=1) | (HasLeft1>=1)) & (!(HasLeft1>=1) | !(HasRight1>=1)))) & G!(Fork1>=1)) | (F(Fork1>=1) & ((HasLeft1>=1) U (((HasRight1>=1) & (HasLeft1>=1)) | (!(HasLeft1>=1) & !(HasRight1>=1))))))
LTLSPEC !(((((Idle0>=1) | !(HasRight0>=1)) & (!(Idle0>=1) | (HasRight0>=1))) | ((Idle1>=1) & !(WaitLeft0>=1))) & ((!(Idle0>=1) & (HasRight0>=1)) | !(Idle1>=1) | ((Idle0>=1) & !(HasRight0>=1)) | (WaitLeft0>=1)))
LTLSPEC !(F((Idle1>=1) | ((!(HasRight1>=1) | !(WaitLeft0>=1)) & ((HasRight1>=1) | (WaitLeft0>=1)))) U (IsEating0>=1))
LTLSPEC !((F!(IsEating1>=1) | (WaitLeft0>=1)) & (!(WaitLeft0>=1) | G(IsEating1>=1)) & G!(WaitRight1>=1))
LTLSPEC !((Idle0>=1) & (((IsEating0>=1) & (HasLeft0>=1)) | (!(HasLeft0>=1) & !(IsEating0>=1))) & F(Fork1>=1))
LTLSPEC !((((G(Fork1>=1) | !(WaitLeft1>=1)) & ((WaitLeft1>=1) | F!(Fork1>=1))) | (WaitRight0>=1)) & ((G(Fork1>=1) & !(WaitLeft1>=1)) | !(WaitRight0>=1) | ((WaitLeft1>=1) & F!(Fork1>=1))))
LTLSPEC !((WaitRight0>=1) V ((Fork1>=1) & (F(WaitRight1>=1) | (HasLeft1>=1))))
LTLSPEC !(F(Fork0>=1) | F(!(Fork1>=1) & !(WaitRight0>=1)))
LTLSPEC !((((HasRight0>=1) V (WaitLeft0>=1)) & ((G(WaitRight0>=1) & (HasRight1>=1)) | (F!(WaitRight0>=1) & !(HasRight1>=1)))) | ((!(HasRight0>=1) U !(WaitLeft0>=1)) & (F!(WaitRight0>=1) | !(HasRight1>=1)) & (G(WaitRight0>=1) | (HasRight1>=1))))
LTLSPEC !((WaitLeft0>=1) & F(F!(HasLeft0>=1) & !(Fork1>=1)))
LTLSPEC !((!(HasRight1>=1) & !(Fork1>=1)) | !(Fork0>=1))
LTLSPEC !(((WaitLeft0>=1) U G(HasLeft0>=1)) U ((Idle0>=1) & (HasLeft1>=1)))
LTLSPEC !(G((F(Idle0>=1) | !(Idle1>=1)) & ((Idle1>=1) | G!(Idle0>=1))))
LTLSPEC !((F(IsEating1>=1) | ((Idle1>=1) & (WaitLeft0>=1))) U (Idle0>=1))
LTLSPEC !((((!(Fork1>=1) & (WaitLeft0>=1)) | !(IsEating0>=1)) & G(HasLeft1>=1)) | (((Fork1>=1) | !(WaitLeft0>=1)) & F!(HasLeft1>=1) & (IsEating0>=1)))
LTLSPEC !((F!(WaitLeft0>=1) | (((Fork0>=1) | !(HasRight1>=1)) & (!(Fork0>=1) | (HasRight1>=1)))) & (G(WaitLeft0>=1) | ((Fork0>=1) & !(HasRight1>=1)) | (!(Fork0>=1) & (HasRight1>=1))))
LTLSPEC !(F((!(HasLeft1>=1) | (WaitRight1>=1)) & (!(WaitRight1>=1) | (HasLeft1>=1))))
LTLSPEC !(((HasRight1>=1) | !(WaitRight1>=1)) V F((HasRight1>=1) U (Idle0>=1)))
LTLSPEC !(F(Idle1>=1) V ((Fork1>=1) & F!(Fork0>=1)))
LTLSPEC !((((Idle1>=1) | G!(IsEating0>=1)) & (HasRight0>=1)) | (F(IsEating0>=1) & !(HasRight0>=1) & !(Idle1>=1)))
LTLSPEC !(G(F!(IsEating1>=1) & F!(WaitLeft1>=1)))
LTLSPEC !(G F((!(WaitLeft0>=1) | !(WaitLeft1>=1)) & ((WaitLeft0>=1) | (WaitLeft1>=1))))
LTLSPEC !((F!(WaitRight0>=1) & G(HasLeft0>=1)) | (F!(HasLeft0>=1) & G(WaitRight0>=1)))
LTLSPEC !(!(WaitLeft1>=1) | (!(Fork0>=1) & G(WaitLeft0>=1)) | (WaitLeft0>=1))
LTLSPEC !(F(((F(Idle1>=1) U (Idle1>=1)) & G(WaitLeft0>=1)) | (F!(WaitLeft0>=1) & (G!(Idle1>=1) V !(Idle1>=1)))))
LTLSPEC !((((Fork1>=1) | F(WaitLeft0>=1)) & !(WaitRight0>=1)) | (G!(WaitLeft0>=1) & !(Fork1>=1) & (WaitRight0>=1)))
LTLSPEC !((F(WaitLeft0>=1) & G F(IsEating1>=1)) | (G!(WaitLeft0>=1) & F G!(IsEating1>=1)))
LTLSPEC !(((((Fork0>=1) & !(WaitRight0>=1)) | (!(Fork0>=1) & (WaitRight0>=1))) & F(HasLeft1>=1)) | (IsEating1>=1))
LTLSPEC !((F!(IsEating0>=1) & G(Idle1>=1) & (WaitLeft0>=1)) | ((!(WaitLeft0>=1) | F!(Idle1>=1)) & G(IsEating0>=1)))
LTLSPEC !(!(Fork1>=1) V (F(WaitLeft0>=1) & G(WaitRight1>=1)))
LTLSPEC !(((Fork0>=1) & (G!(IsEating1>=1) V (!(Fork0>=1) | !(WaitRight1>=1)))) | (!(Fork0>=1) & (F(IsEating1>=1) U ((Fork0>=1) & (WaitRight1>=1)))))
LTLSPEC !(((HasRight0>=1) & (IsEating0>=1)) | (!(HasRight0>=1) & !(IsEating0>=1)))
LTLSPEC !(G(((WaitRight0>=1) & (G F(HasLeft0>=1) | (HasLeft0>=1))) | (!(HasLeft0>=1) & F G!(HasLeft0>=1) & !(WaitRight0>=1))))
LTLSPEC !(F(F!(WaitLeft0>=1) V (!(Idle1>=1) V !(HasLeft0>=1))))
LTLSPEC !((G!(HasRight1>=1) & !(IsEating0>=1)) | (!(Idle0>=1) & !(Idle1>=1)) | ((Idle0>=1) & (Idle1>=1)) | (F(HasRight1>=1) & (IsEating0>=1)))
LTLSPEC !((!(HasRight0>=1) | (HasRight1>=1)) & G(((WaitRight1>=1) & (HasLeft1>=1)) | (!(HasLeft1>=1) & !(WaitRight1>=1))))
LTLSPEC !(F(HasLeft1>=1) U (!(WaitLeft1>=1) | F!(Fork1>=1)))
LTLSPEC !(((F(IsEating0>=1) U (IsEating0>=1)) U (WaitRight1>=1)) V (WaitRight0>=1))
LTLSPEC !((F(HasLeft0>=1) | ((HasRight0>=1) V !(HasRight1>=1))) & ((!(HasRight0>=1) U (HasRight1>=1)) | G!(HasLeft0>=1)))
LTLSPEC !(((Fork1>=1) & F(!(HasLeft1>=1) U !(IsEating0>=1))) | (!(Fork1>=1) & G(IsEating0>=1)))
LTLSPEC !(G(F!(WaitLeft1>=1) & F G!(Idle0>=1)))
LTLSPEC !(((!(Idle0>=1) | (HasLeft1>=1)) & ((Idle0>=1) | !(HasLeft1>=1))) V (IsEating0>=1))
LTLSPEC !(((WaitRight0>=1) & (WaitRight1>=1)) | (WaitLeft1>=1) | F!(Fork1>=1))
LTLSPEC !(((((WaitRight0>=1) & (WaitLeft1>=1)) | (!(WaitLeft1>=1) & !(WaitRight0>=1))) & !(Fork0>=1)) | ((Fork0>=1) & (!(WaitLeft1>=1) | !(WaitRight0>=1)) & ((WaitRight0>=1) | (WaitLeft1>=1))))
LTLSPEC !(F((G(Fork1>=1) & ((Fork0>=1) U (HasLeft0>=1))) | ((!(Fork0>=1) V !(HasLeft0>=1)) & F!(Fork1>=1))))
LTLSPEC !((((WaitRight0>=1) V (HasRight0>=1)) & (G!(Fork0>=1) V !(WaitRight1>=1))) | ((F(Fork0>=1) U (WaitRight1>=1)) & (!(WaitRight0>=1) U !(HasRight0>=1))))
LTLSPEC !(G!(HasLeft1>=1) | (F(WaitLeft1>=1) & G(WaitRight0>=1)) | (F!(WaitRight0>=1) & G!(WaitLeft1>=1)))
LTLSPEC !((!(HasLeft1>=1) & ((F(Idle0>=1) & !(WaitLeft1>=1)) | !(IsEating0>=1) | (G!(Idle0>=1) & (WaitLeft1>=1))) & (((G!(Idle0>=1) | (WaitLeft1>=1)) & (F(Idle0>=1) | !(WaitLeft1>=1))) | (IsEating0>=1))) | ((((G!(Idle0>=1) | (WaitLeft1>=1)) & (IsEating0>=1) & (F(Idle0>=1) | !(WaitLeft1>=1))) | (!(IsEating0>=1) & ((F(Idle0>=1) & !(WaitLeft1>=1)) | (G!(Idle0>=1) & (WaitLeft1>=1))))) & (HasLeft1>=1)))
LTLSPEC !(F(F(F(WaitRight1>=1) & (WaitLeft0>=1)) V (IsEating0>=1)))
LTLSPEC !((F!(WaitRight1>=1) | F(!(Fork1>=1) | !(WaitRight0>=1))) & (G((Fork1>=1) & (WaitRight0>=1)) | G(WaitRight1>=1)))
LTLSPEC !((((!(WaitLeft1>=1) & (HasRight0>=1)) | (!(HasRight0>=1) & (WaitLeft1>=1))) & !(HasRight1>=1)) | (WaitLeft1>=1) | ((!(HasRight0>=1) | (WaitLeft1>=1)) & (HasRight1>=1) & (!(WaitLeft1>=1) | (HasRight0>=1))))
LTLSPEC !(F(WaitLeft1>=1) | (!(WaitRight1>=1) V !(HasRight0>=1)))
LTLSPEC !((F!(IsEating1>=1) & (F(HasLeft1>=1) U !(Idle1>=1))) | (G(IsEating1>=1) & (G!(HasLeft1>=1) V (Idle1>=1))))
LTLSPEC !((!(HasRight0>=1) & (((Idle1>=1) & F((!(HasLeft0>=1) | !(WaitLeft0>=1)) & ((WaitLeft0>=1) | (HasLeft0>=1)))) | (!(Idle1>=1) & G(((WaitLeft0>=1) & (HasLeft0>=1)) | (!(HasLeft0>=1) & !(WaitLeft0>=1)))))) | (((Idle1>=1) | F((!(HasLeft0>=1) | !(WaitLeft0>=1)) & ((WaitLeft0>=1) | (HasLeft0>=1)))) & (HasRight0>=1) & (!(Idle1>=1) | G(((WaitLeft0>=1) & (HasLeft0>=1)) | (!(HasLeft0>=1) & !(WaitLeft0>=1))))))
LTLSPEC !((((!(WaitRight0>=1) V !(Idle1>=1)) | !(Fork0>=1)) & ((Fork0>=1) | ((WaitRight0>=1) U (Idle1>=1)))) | (Idle1>=1))
LTLSPEC !(G((F G!(HasRight1>=1) & (HasRight1>=1)) | (!(HasRight1>=1) & G F(HasRight1>=1))))
LTLSPEC !(F G((HasLeft1>=1) U ((Idle0>=1) | G!(IsEating0>=1))))
LTLSPEC !(((Fork0>=1) & G(WaitRight1>=1) & (!(WaitLeft1>=1) | (HasLeft0>=1))) | ((!(Fork0>=1) | (!(HasLeft0>=1) & (WaitLeft1>=1))) & F!(WaitRight1>=1)))
LTLSPEC !(((!(Idle0>=1) & (!(Idle1>=1) V !(WaitLeft0>=1))) | ((Idle0>=1) & ((Idle1>=1) U (WaitLeft0>=1)))) & !(HasRight0>=1))
LTLSPEC !((((Fork1>=1) & (WaitLeft1>=1)) | (!(WaitLeft1>=1) & !(Fork1>=1))) U (!(Fork0>=1) | (HasRight1>=1)))
LTLSPEC !((((Fork1>=1) | !(IsEating1>=1)) & F!(HasLeft1>=1) & (!(Fork1>=1) | (IsEating1>=1))) | (((!(Fork1>=1) & (IsEating1>=1)) | ((Fork1>=1) & !(IsEating1>=1))) & G(HasLeft1>=1)))
LTLSPEC !((F(WaitRight1>=1) & F!(Idle0>=1)) | (G(Idle0>=1) & G!(WaitRight1>=1)))
LTLSPEC !((((WaitRight0>=1) V !(Idle1>=1)) & F!(Idle0>=1)) | (G(Idle0>=1) & (!(WaitRight0>=1) U (Idle1>=1))))
LTLSPEC !(G(((HasRight1>=1) & (HasLeft0>=1)) | (!(HasLeft0>=1) & !(HasRight1>=1)) | G(WaitLeft0>=1)))
Examples/philo/.svn/text-base/formula.ltl.svn-base deleted 100644 → 0
+ 0
− 100
View file @ 3d0bb53a
G(!"Fork1" & !WaitRight0) & !HasRight1
(Idle1 & (HasRight1 U !HasLeft1)) | HasRight1 | (!Idle1 & (!HasRight1 R HasLeft1))
((F!IsEating0 & HasLeft1) | (!HasLeft1 & GIsEating0)) U Idle1
(!WaitRight0 R Idle1) R F!IsEating1
(G!Idle1 & F((!WaitLeft1 & HasRight0) | (!HasRight0 & WaitLeft1))) | (FIdle1 & G((!HasRight0 | WaitLeft1) & (!WaitLeft1 | HasRight0)))
(IsEating1 & (((!"Fork1" U HasLeft0) & WaitLeft0) | (("Fork1" R !HasLeft0) & !WaitLeft0))) | (!IsEating1 & (("Fork1" R !HasLeft0) | !WaitLeft0) & ((!"Fork1" U HasLeft0) | WaitLeft0))
((G!WaitLeft0 | !"Fork1") & ("Fork1" | FWaitLeft0) & WaitRight1) | (((G!WaitLeft0 & !"Fork1") | ("Fork1" & FWaitLeft0)) & !WaitRight1)
F((((GIsEating1 & G!WaitRight0) | (F!IsEating1 & FWaitRight0)) & HasLeft1) | (!HasLeft1 & (GIsEating1 | G!WaitRight0) & (F!IsEating1 | FWaitRight0)))
(!IsEating0 & (("Fork1" & HasRight0 & HasRight1) | (!HasRight1 & (!HasRight0 | !"Fork1")))) | (IsEating0 & (!HasRight0 | !HasRight1 | !"Fork1") & (("Fork1" & HasRight0) | HasRight1))
FHasRight0 & (FWaitLeft0 | FHasLeft1)
(Idle0 & G!HasLeft0) | (!"Fork0" & !Idle0) | ("Fork0" & Idle0)
((F!Idle0 R (!IsEating0 | !WaitRight0)) & WaitRight0) | ((GIdle0 U (WaitRight0 & IsEating0)) & !WaitRight0)
((!HasRight1 & !WaitLeft0) | (HasRight1 & WaitLeft0)) R (FWaitLeft0 | IsEating0)
(F(!Idle0 | WaitRight0) & (!"Fork1" | WaitLeft1)) | ("Fork1" & G(Idle0 & !WaitRight0) & !WaitLeft1)
G((!IsEating1 & !"Fork0" & WaitLeft0) | (!WaitLeft0 & ("Fork0" | IsEating1)))
(FHasRight0 & G!Idle1) | (G!HasRight0 & FIdle1)
GIdle1 & (F!HasRight0 | !Idle1)
(WaitRight1 | HasLeft1) & ((FIsEating0 & IsEating1) | (G!IsEating0 & !IsEating1))
FWaitRight1 U ((!WaitLeft1 & ((Idle0 & !HasLeft1) | (!Idle0 & HasLeft1))) | ((!Idle0 | HasLeft1) & WaitLeft1 & (Idle0 | !HasLeft1)))
(Idle0 & (!HasRight1 | (G!WaitLeft0 U !Idle0)) & ((FWaitLeft0 R Idle0) | HasRight1)) | (!Idle0 & ((!HasRight1 & (G!WaitLeft0 U !Idle0)) | ((FWaitLeft0 R Idle0) & HasRight1)))
((WaitLeft0 U "Fork1") & GHasRight0) | (F!HasRight0 & (!WaitLeft0 R !"Fork1"))
(!Idle0 & ("Fork0" | WaitRight1) & (!"Fork0" | !WaitRight1)) | (Idle0 & (("Fork0" & WaitRight1) | (!"Fork0" & !WaitRight1)))
F(Idle0 | (!HasLeft1 & (Idle1 U "Fork0")) | ((!Idle1 R !"Fork0") & HasLeft1))
("Fork1" & !HasLeft1 & G!WaitLeft0) | ((FWaitLeft0 | !"Fork1") & HasLeft1)
(((GIsEating0 & FHasLeft1) | (F!IsEating0 & G!HasLeft1)) & GHasRight0) | (F!HasRight0 & (F!IsEating0 | G!HasLeft1) & (GIsEating0 | FHasLeft1))
Idle1 & ("Fork0" | (FHasRight1 & !"Fork1"))
(!WaitLeft0 | HasRight0) U ((!HasRight0 & !WaitRight1) | (WaitRight1 & HasRight0))
(FGHasLeft1 & (G!WaitRight1 R !WaitLeft1)) | ((FWaitRight1 U WaitLeft1) & GF!HasLeft1)
F!WaitRight0 | ("Fork0" & FWaitLeft0) | (G!WaitLeft0 & !"Fork0")
!IsEating0 | ("Fork1" & F!"Fork1")
F((Idle0 & (!"Fork1" U !HasRight1) & IsEating1) | (!Idle0 & (("Fork1" R HasRight1) | !IsEating1)))
F(((F!WaitRight1 | HasRight1) & (!HasRight1 | GWaitRight1)) R !IsEating1)
(!HasRight0 & GWaitRight1) | (F!WaitRight1 & HasRight0)
F((!HasLeft0 & !WaitRight0) | (WaitRight0 & HasLeft0)) U !Idle0
(!HasLeft0 | WaitLeft0) R (!"Fork0" | HasRight1)
(!HasRight0 & (("Fork1" U "Fork0") R !HasRight1)) | (((!"Fork1" R !"Fork0") U HasRight1) & HasRight0)
((!HasLeft1 R ((HasRight1 | HasLeft1) & (!HasLeft1 | !HasRight1))) & G!"Fork1") | (F"Fork1" & (HasLeft1 U ((HasRight1 & HasLeft1) | (!HasLeft1 & !HasRight1))))
(((Idle0 | !HasRight0) & (!Idle0 | HasRight0)) | (Idle1 & !WaitLeft0)) & ((!Idle0 & HasRight0) | !Idle1 | (Idle0 & !HasRight0) | WaitLeft0)
F(Idle1 | ((!HasRight1 | !WaitLeft0) & (HasRight1 | WaitLeft0))) U IsEating0
(F!IsEating1 | WaitLeft0) & (!WaitLeft0 | GIsEating1) & G!WaitRight1
Idle0 & ((IsEating0 & HasLeft0) | (!HasLeft0 & !IsEating0)) & F"Fork1"
(((G"Fork1" | !WaitLeft1) & (WaitLeft1 | F!"Fork1")) | WaitRight0) & ((G"Fork1" & !WaitLeft1) | !WaitRight0 | (WaitLeft1 & F!"Fork1"))
WaitRight0 R ("Fork1" & (FWaitRight1 | HasLeft1))
F"Fork0" | F(!"Fork1" & !WaitRight0)
((HasRight0 R WaitLeft0) & ((GWaitRight0 & HasRight1) | (F!WaitRight0 & !HasRight1))) | ((!HasRight0 U !WaitLeft0) & (F!WaitRight0 | !HasRight1) & (GWaitRight0 | HasRight1))
WaitLeft0 & F(F!HasLeft0 & !"Fork1")
(!HasRight1 & !"Fork1") | !"Fork0"
(WaitLeft0 U GHasLeft0) U (Idle0 & HasLeft1)
G((FIdle0 | !Idle1) & (Idle1 | G!Idle0))
(FIsEating1 | (Idle1 & WaitLeft0)) U Idle0
(((!"Fork1" & WaitLeft0) | !IsEating0) & GHasLeft1) | (("Fork1" | !WaitLeft0) & F!HasLeft1 & IsEating0)
(F!WaitLeft0 | (("Fork0" | !HasRight1) & (!"Fork0" | HasRight1))) & (GWaitLeft0 | ("Fork0" & !HasRight1) | (!"Fork0" & HasRight1))
F((!HasLeft1 | WaitRight1) & (!WaitRight1 | HasLeft1))
(HasRight1 | !WaitRight1) R F(HasRight1 U Idle0)
FIdle1 R ("Fork1" & F!"Fork0")
((Idle1 | G!IsEating0) & HasRight0) | (FIsEating0 & !HasRight0 & !Idle1)
G(F!IsEating1 & F!WaitLeft1)
GF((!WaitLeft0 | !WaitLeft1) & (WaitLeft0 | WaitLeft1))
(F!WaitRight0 & GHasLeft0) | (F!HasLeft0 & GWaitRight0)
!WaitLeft1 | (!"Fork0" & GWaitLeft0) | WaitLeft0
F(((FIdle1 U Idle1) & GWaitLeft0) | (F!WaitLeft0 & (G!Idle1 R !Idle1)))
(("Fork1" | FWaitLeft0) & !WaitRight0) | (G!WaitLeft0 & !"Fork1" & WaitRight0)
(FWaitLeft0 & GFIsEating1) | (G!WaitLeft0 & FG!IsEating1)
((("Fork0" & !WaitRight0) | (!"Fork0" & WaitRight0)) & FHasLeft1) | IsEating1
(F!IsEating0 & GIdle1 & WaitLeft0) | ((!WaitLeft0 | F!Idle1) & GIsEating0)
!"Fork1" R (FWaitLeft0 & GWaitRight1)
("Fork0" & (G!IsEating1 R (!"Fork0" | !WaitRight1))) | (!"Fork0" & (FIsEating1 U ("Fork0" & WaitRight1)))
(HasRight0 & IsEating0) | (!HasRight0 & !IsEating0)
G((WaitRight0 & (GFHasLeft0 | HasLeft0)) | (!HasLeft0 & FG!HasLeft0 & !WaitRight0))
F(F!WaitLeft0 R (!Idle1 R !HasLeft0))
(G!HasRight1 & !IsEating0) | (!Idle0 & !Idle1) | (Idle0 & Idle1) | (FHasRight1 & IsEating0)
(!HasRight0 | HasRight1) & G((WaitRight1 & HasLeft1) | (!HasLeft1 & !WaitRight1))
FHasLeft1 U (!WaitLeft1 | F!"Fork1")
((FIsEating0 U IsEating0) U WaitRight1) R WaitRight0
(FHasLeft0 | (HasRight0 R !HasRight1)) & ((!HasRight0 U HasRight1) | G!HasLeft0)
("Fork1" & F(!HasLeft1 U !IsEating0)) | (!"Fork1" & GIsEating0)
G(F!WaitLeft1 & FG!Idle0)
((!Idle0 | HasLeft1) & (Idle0 | !HasLeft1)) R IsEating0
(WaitRight0 & WaitRight1) | WaitLeft1 | F!"Fork1"
(((WaitRight0 & WaitLeft1) | (!WaitLeft1 & !WaitRight0)) & !"Fork0") | ("Fork0" & (!WaitLeft1 | !WaitRight0) & (WaitRight0 | WaitLeft1))
F((G"Fork1" & ("Fork0" U HasLeft0)) | ((!"Fork0" R !HasLeft0) & F!"Fork1"))
((WaitRight0 R HasRight0) & (G!"Fork0" R !WaitRight1)) | ((F"Fork0" U WaitRight1) & (!WaitRight0 U !HasRight0))
G!HasLeft1 | (FWaitLeft1 & GWaitRight0) | (F!WaitRight0 & G!WaitLeft1)
(!HasLeft1 & ((FIdle0 & !WaitLeft1) | !IsEating0 | (G!Idle0 & WaitLeft1)) & (((G!Idle0 | WaitLeft1) & (FIdle0 | !WaitLeft1)) | IsEating0)) | ((((G!Idle0 | WaitLeft1) & IsEating0 & (FIdle0 | !WaitLeft1)) | (!IsEating0 & ((FIdle0 & !WaitLeft1) | (G!Idle0 & WaitLeft1)))) & HasLeft1)
F(F(FWaitRight1 & WaitLeft0) R IsEating0)
(F!WaitRight1 | F(!"Fork1" | !WaitRight0)) & (G("Fork1" & WaitRight0) | GWaitRight1)
(((!WaitLeft1 & HasRight0) | (!HasRight0 & WaitLeft1)) & !HasRight1) | WaitLeft1 | ((!HasRight0 | WaitLeft1) & HasRight1 & (!WaitLeft1 | HasRight0))
FWaitLeft1 | (!WaitRight1 R !HasRight0)
(F!IsEating1 & (FHasLeft1 U !Idle1)) | (GIsEating1 & (G!HasLeft1 R Idle1))
(!HasRight0 & ((Idle1 & F((!HasLeft0 | !WaitLeft0) & (WaitLeft0 | HasLeft0))) | (!Idle1 & G((WaitLeft0 & HasLeft0) | (!HasLeft0 & !WaitLeft0))))) | ((Idle1 | F((!HasLeft0 | !WaitLeft0) & (WaitLeft0 | HasLeft0))) & HasRight0 & (!Idle1 | G((WaitLeft0 & HasLeft0) | (!HasLeft0 & !WaitLeft0))))
(((!WaitRight0 R !Idle1) | !"Fork0") & ("Fork0" | (WaitRight0 U Idle1))) | Idle1
G((FG!HasRight1 & HasRight1) | (!HasRight1 & GFHasRight1))
FG(HasLeft1 U (Idle0 | G!IsEating0))
("Fork0" & GWaitRight1 & (!WaitLeft1 | HasLeft0)) | ((!"Fork0" | (!HasLeft0 & WaitLeft1)) & F!WaitRight1)
((!Idle0 & (!Idle1 R !WaitLeft0)) | (Idle0 & (Idle1 U WaitLeft0))) & !HasRight0
(("Fork1" & WaitLeft1) | (!WaitLeft1 & !"Fork1")) U (!"Fork0" | HasRight1)
(("Fork1" | !IsEating1) & F!HasLeft1 & (!"Fork1" | IsEating1)) | (((!"Fork1" & IsEating1) | ("Fork1" & !IsEating1)) & GHasLeft1)
(FWaitRight1 & F!Idle0) | (GIdle0 & G!WaitRight1)
((WaitRight0 R !Idle1) & F!Idle0) | (GIdle0 & (!WaitRight0 U Idle1))
G((HasRight1 & HasLeft0) | (!HasLeft0 & !HasRight1) | GWaitLeft0)
Examples/philo/.svn/text-base/mctest.sh.svn-base deleted 100644 → 0
+ 0
− 24
View file @ 3d0bb53a
#!/bin/sh
set -e
RANDLTL=/home/dp/spot/src/ltltest/randltl
CHECKSOG=/home/dp/checksog-state/check-sog
CHECKPN=/home/dp/checkpn-0.0b/src/checkpn
TIME='/usr/bin/time -p'
MODEL='philo6.net'
BOUND='1'
$RANDLTL -p 'X=0.0' -F 10000 -u -s 1 -f 5 -r 5 `cat philo.ap` |
while read f; do
echo formula $f
$CHECKSOG -aCou99 -c -f"$f" $MODEL $BOUND | grep accepting > sog.res
$CHECKPN -f"$f" $MODEL | grep accepting > pn.res
mavar=`diff sog.res pn.res | wc -l`
if [ $mavar -ne 0 ]
then
echo bug with $f
exit 0
fi
rm sog.res pn.res
done
Examples/philo/.svn/text-base/philo.ap.svn-base deleted 100644 → 0
+ 0
− 14
View file @ 3d0bb53a
Idle0
WaitLeft0
HasLeft0
WaitRight0
HasRight0
Fork0
IsEating0
Idle1
WaitLeft1
HasLeft1
WaitRight1
HasRight1
Fork1
IsEating1
Examples/philo/.svn/text-base/philo.sed.org.svn-base deleted 100644 → 0
+ 0
− 22
View file @ 3d0bb53a
s/^/LTLSPEC !(/g
s/$/)/g
s/Idle0/(Idle0>=1)/g
s/WaitLeft0/(WaitLeft0>=1)/g
s/HasLeft0/(HasLeft0>=1)/g
s/WaitRight0/(WaitRight0>=1)/g
s/HasRight0/(HasRight0>=1)/g
s/Fork0/(Fork0>=1)/g
s/IsEating0/(IsEating0>=1)/g
s/Idle1/(Idle1>=1)/g
s/WaitLeft1/(WaitLeft1>=1)/g
s/HasLeft1/(HasLeft1>=1)/g
s/WaitRight1/(WaitRight1>=1)/g
s/HasRight1/(HasRight1>=1)/g
s/Fork1/(Fork1>=1)/g
s/IsEating1/(IsEating1>=1)/g
s/ R / V /g
s/FG/F G/g
s/GF/G F/g
s/"//g
Examples/philo/.svn/text-base/philo.sed.svn-base deleted 100644 → 0
+ 0
− 15
View file @ 3d0bb53a
s/^/LTLSPEC !(/g
s/$/)/g
s/Idle\([0-9][0-9]*\)/(Idle\1>=1)/g
s/WaitLeft\([0-9][0-9]*\)/(WaitLeft\1>=1)/g
s/HasLeft\([0-9][0-9]*\)/(HasLeft\1>=1)/g
s/WaitRight\([0-9][0-9]*\)/(WaitRight\1>=1)/g
s/HasRight\([0-9][0-9]*\)/(HasRight\1>=1)/g
s/Fork\([0-9][0-9]*\)/(Fork\1>=1)/g
s/IsEating\([0-9][0-9]*\)/(IsEating\1>=1)/g
s/ R / V /g
s/FG/F G/g
s/GF/G F/g
s/"//g
Examples/philo/.svn/text-base/philo10.net.ltl.smv.svn-base deleted 100644 → 0
+ 0
− 10
View file @ 3d0bb53a
LTLSPEC !(G(!(Fork9>=1) & !(WaitRight4>=1)) & !(HasRight9>=1))
LTLSPEC !((HasRight5>=1) | ((Idle5>=1) & ((HasRight7>=1) U !(HasLeft9>=1))) | (!(Idle5>=1) & (!(HasRight7>=1) V (HasLeft9>=1))))
LTLSPEC !(((!(HasLeft5>=1) & G(IsEating2>=1)) | (F!(IsEating2>=1) & (HasLeft5>=1))) U (Idle8>=1))
LTLSPEC !((!(WaitRight3>=1) V (Idle6>=1)) V F!(IsEating5>=1))
LTLSPEC !((((HasRight1>=1) U ((!(HasRight3>=1) & (WaitLeft9>=1)) | (!(WaitLeft9>=1) & (HasRight3>=1)))) & F!(Idle2>=1)) | (G(Idle2>=1) & (!(HasRight1>=1) V ((!(WaitLeft9>=1) | (HasRight3>=1)) & (!(HasRight3>=1) | (WaitLeft9>=1))))))
LTLSPEC !((((((Fork9>=1) V !(HasLeft1>=1)) & !(WaitLeft1>=1)) | ((!(Fork9>=1) U (HasLeft1>=1)) & (WaitLeft1>=1))) & (IsEating6>=1)) | (!(IsEating6>=1) & (((Fork9>=1) V !(HasLeft1>=1)) | !(WaitLeft1>=1)) & ((!(Fork9>=1) U (HasLeft1>=1)) | (WaitLeft1>=1))))
LTLSPEC !(G(IsEating3>=1) & (G!(IsEating3>=1) | !(WaitLeft4>=1)))
LTLSPEC !(F((!(HasLeft5>=1) & (F!(IsEating8>=1) | F(WaitRight3>=1)) & (G(IsEating8>=1) | G!(WaitRight3>=1))) | (((G(IsEating8>=1) & G!(WaitRight3>=1)) | (F!(IsEating8>=1) & F(WaitRight3>=1))) & (HasLeft5>=1))))
LTLSPEC !(F((!(Fork1>=1) & (IsEating2>=1)) | ((Fork1>=1) & !(IsEating2>=1))) | (!(Fork2>=1) U !(WaitRight7>=1)))
LTLSPEC !(F(HasRight2>=1) & (F(WaitLeft1>=1) | F(HasLeft6>=1)))
Examples/philo/.svn/text-base/philo10.net.ltl.svn-base deleted 100644 → 0
+ 0
− 10
View file @ 3d0bb53a
G(!"Fork9" & !WaitRight4) & !HasRight9
HasRight5 | (Idle5 & (HasRight7 U !HasLeft9)) | (!Idle5 & (!HasRight7 R HasLeft9))
((!HasLeft5 & GIsEating2) | (F!IsEating2 & HasLeft5)) U Idle8
(!WaitRight3 R Idle6) R F!IsEating5
((HasRight1 U ((!HasRight3 & WaitLeft9) | (!WaitLeft9 & HasRight3))) & F!Idle2) | (GIdle2 & (!HasRight1 R ((!WaitLeft9 | HasRight3) & (!HasRight3 | WaitLeft9))))
(((("Fork9" R !HasLeft1) & !WaitLeft1) | ((!"Fork9" U HasLeft1) & WaitLeft1)) & IsEating6) | (!IsEating6 & (("Fork9" R !HasLeft1) | !WaitLeft1) & ((!"Fork9" U HasLeft1) | WaitLeft1))
GIsEating3 & (G!IsEating3 | !WaitLeft4)
F((!HasLeft5 & (F!IsEating8 | FWaitRight3) & (GIsEating8 | G!WaitRight3)) | (((GIsEating8 & G!WaitRight3) | (F!IsEating8 & FWaitRight3)) & HasLeft5))
F((!"Fork1" & IsEating2) | ("Fork1" & !IsEating2)) | (!"Fork2" U !WaitRight7)
FHasRight2 & (FWaitLeft1 | FHasLeft6)
Examples/philo/.svn/text-base/philo10.net.smv.svn-base deleted 100644 → 0
+ 0
− 3923
View file @ 3d0bb53a
This diff is collapsed.
Examples/philo/.svn/text-base/philo10.net.svn-base deleted 100644 → 0
+ 0
− 270
View file @ 3d0bb53a
#place Idle0 mk(<..>)
#place WaitLeft0
#place HasLeft0
#place WaitRight0
#place HasRight0
#place Fork0 mk(<..>)
#place IsEating0
#place Idle1 mk(<..>)
#place WaitLeft1
#place HasLeft1
#place WaitRight1
#place HasRight1
#place Fork1 mk(<..>)
#place IsEating1
#place Idle2 mk(<..>)
#place WaitLeft2
#place HasLeft2
#place WaitRight2
#place HasRight2
#place Fork2 mk(<..>)
#place IsEating2
#place Idle3 mk(<..>)
#place WaitLeft3
#place HasLeft3
#place WaitRight3
#place HasRight3
#place Fork3 mk(<..>)
#place IsEating3
#place Idle4 mk(<..>)
#place WaitLeft4
#place HasLeft4
#place WaitRight4
#place HasRight4
#place Fork4 mk(<..>)
#place IsEating4
#place Idle5 mk(<..>)
#place WaitLeft5
#place HasLeft5
#place WaitRight5
#place HasRight5
#place Fork5 mk(<..>)
#place IsEating5
#place Idle6 mk(<..>)
#place WaitLeft6
#place HasLeft6
#place WaitRight6
#place HasRight6
#place Fork6 mk(<..>)
#place IsEating6
#place Idle7 mk(<..>)
#place WaitLeft7
#place HasLeft7
#place WaitRight7
#place HasRight7
#place Fork7 mk(<..>)
#place IsEating7
#place Idle8 mk(<..>)
#place WaitLeft8
#place HasLeft8
#place WaitRight8
#place HasRight8
#place Fork8 mk(<..>)
#place IsEating8
#place Idle9 mk(<..>)
#place WaitLeft9
#place HasLeft9
#place WaitRight9
#place HasRight9
#place Fork9 mk(<..>)
#place IsEating9
#trans GoEat0
in {Idle0:<..>;}
out {WaitLeft0:<..>;WaitRight0:<..>;}
#endtr
#trans GoLeft0
in {Fork9:<..>;WaitLeft0:<..>;}
out {HasLeft0:<..>;}
#endtr
#trans GoRight0
in {Fork0:<..>;WaitRight0:<..>;}
out {HasRight0:<..>;}
#endtr
#trans Eat0
in {HasLeft0:<..>;HasRight0:<..>;}
out {IsEating0:<..>;}
#endtr
#trans Release0
in {IsEating0:<..>;}
out {Idle0:<..>;Fork9:<..>;Fork0:<..>;}
#endtr
#trans GoEat1
in {Idle1:<..>;}
out {WaitLeft1:<..>;WaitRight1:<..>;}
#endtr
#trans GoLeft1
in {Fork0:<..>;WaitLeft1:<..>;}
out {HasLeft1:<..>;}
#endtr
#trans GoRight1
in {Fork1:<..>;WaitRight1:<..>;}
out {HasRight1:<..>;}
#endtr
#trans Eat1
in {HasLeft1:<..>;HasRight1:<..>;}
out {IsEating1:<..>;}
#endtr
#trans Release1
in {IsEating1:<..>;}
out {Idle1:<..>;Fork0:<..>;Fork1:<..>;}
#endtr
#trans GoEat2
in {Idle2:<..>;}
out {WaitLeft2:<..>;WaitRight2:<..>;}
#endtr
#trans GoLeft2
in {Fork1:<..>;WaitLeft2:<..>;}
out {HasLeft2:<..>;}
#endtr
#trans GoRight2
in {Fork2:<..>;WaitRight2:<..>;}
out {HasRight2:<..>;}
#endtr
#trans Eat2
in {HasLeft2:<..>;HasRight2:<..>;}
out {IsEating2:<..>;}
#endtr
#trans Release2
in {IsEating2:<..>;}
out {Idle2:<..>;Fork1:<..>;Fork2:<..>;}
#endtr
#trans GoEat3
in {Idle3:<..>;}
out {WaitLeft3:<..>;WaitRight3:<..>;}
#endtr
#trans GoLeft3
in {Fork2:<..>;WaitLeft3:<..>;}
out {HasLeft3:<..>;}
#endtr
#trans GoRight3
in {Fork3:<..>;WaitRight3:<..>;}
out {HasRight3:<..>;}
#endtr
#trans Eat3
in {HasLeft3:<..>;HasRight3:<..>;}
out {IsEating3:<..>;}
#endtr
#trans Release3
in {IsEating3:<..>;}
out {Idle3:<..>;Fork2:<..>;Fork3:<..>;}
#endtr
#trans GoEat4
in {Idle4:<..>;}
out {WaitLeft4:<..>;WaitRight4:<..>;}
#endtr
#trans GoLeft4
in {Fork3:<..>;WaitLeft4:<..>;}
out {HasLeft4:<..>;}
#endtr
#trans GoRight4
in {Fork4:<..>;WaitRight4:<..>;}
out {HasRight4:<..>;}
#endtr
#trans Eat4
in {HasLeft4:<..>;HasRight4:<..>;}
out {IsEating4:<..>;}
#endtr
#trans Release4
in {IsEating4:<..>;}
out {Idle4:<..>;Fork3:<..>;Fork4:<..>;}
#endtr
#trans GoEat5
in {Idle5:<..>;}
out {WaitLeft5:<..>;WaitRight5:<..>;}
#endtr
#trans GoLeft5
in {Fork4:<..>;WaitLeft5:<..>;}
out {HasLeft5:<..>;}
#endtr
#trans GoRight5
in {Fork5:<..>;WaitRight5:<..>;}
out {HasRight5:<..>;}
#endtr
#trans Eat5
in {HasLeft5:<..>;HasRight5:<..>;}
out {IsEating5:<..>;}
#endtr
#trans Release5
in {IsEating5:<..>;}
out {Idle5:<..>;Fork4:<..>;Fork5:<..>;}
#endtr
#trans GoEat6
in {Idle6:<..>;}
out {WaitLeft6:<..>;WaitRight6:<..>;}
#endtr
#trans GoLeft6
in {Fork5:<..>;WaitLeft6:<..>;}
out {HasLeft6:<..>;}
#endtr
#trans GoRight6
in {Fork6:<..>;WaitRight6:<..>;}
out {HasRight6:<..>;}
#endtr
#trans Eat6
in {HasLeft6:<..>;HasRight6:<..>;}
out {IsEating6:<..>;}
#endtr
#trans Release6
in {IsEating6:<..>;}
out {Idle6:<..>;Fork5:<..>;Fork6:<..>;}
#endtr
#trans GoEat7
in {Idle7:<..>;}
out {WaitLeft7:<..>;WaitRight7:<..>;}
#endtr
#trans GoLeft7
in {Fork6:<..>;WaitLeft7:<..>;}
out {HasLeft7:<..>;}
#endtr
#trans GoRight7
in {Fork7:<..>;WaitRight7:<..>;}
out {HasRight7:<..>;}
#endtr
#trans Eat7
in {HasLeft7:<..>;HasRight7:<..>;}
out {IsEating7:<..>;}
#endtr
#trans Release7
in {IsEating7:<..>;}
out {Idle7:<..>;Fork6:<..>;Fork7:<..>;}
#endtr
#trans GoEat8
in {Idle8:<..>;}
out {WaitLeft8:<..>;WaitRight8:<..>;}
#endtr
#trans GoLeft8
in {Fork7:<..>;WaitLeft8:<..>;}
out {HasLeft8:<..>;}
#endtr
#trans GoRight8
in {Fork8:<..>;WaitRight8:<..>;}
out {HasRight8:<..>;}
#endtr
#trans Eat8
in {HasLeft8:<..>;HasRight8:<..>;}
out {IsEating8:<..>;}
#endtr
#trans Release8
in {IsEating8:<..>;}
out {Idle8:<..>;Fork7:<..>;Fork8:<..>;}
#endtr
#trans GoEat9
in {Idle9:<..>;}
out {WaitLeft9:<..>;WaitRight9:<..>;}
#endtr
#trans GoLeft9
in {Fork8:<..>;WaitLeft9:<..>;}
out {HasLeft9:<..>;}
#endtr
#trans GoRight9
in {Fork9:<..>;WaitRight9:<..>;}
out {HasRight9:<..>;}
#endtr
#trans Eat9
in {HasLeft9:<..>;HasRight9:<..>;}
out {IsEating9:<..>;}
#endtr
#trans Release9
in {IsEating9:<..>;}
out {Idle9:<..>;Fork8:<..>;Fork9:<..>;}
#endtr
Examples/philo/.svn/text-base/philo100.net.ltl.svn-base deleted 100644 → 0
+ 0
− 10
View file @ 3d0bb53a
G(!"Fork57" & !WaitRight16) & !HasRight68
((!HasRight46 R HasLeft5) & !Idle18) | (Idle18 & (HasRight46 U !HasLeft5)) | HasRight27
((F!HasRight99 & HasRight5) | (!HasRight5 & GHasRight99)) U Idle56
(!Idle99 R Idle27) R F!WaitLeft28
(F!"Fork88" & (WaitRight87 U ((!HasLeft56 & HasRight11) | (!HasRight11 & HasLeft56)))) | (G"Fork88" & (!WaitRight87 R ((!HasLeft56 | HasRight11) & (!HasRight11 | HasLeft56))))
(((WaitLeft89 & (!"Fork57" U HasLeft75)) | (!WaitLeft89 & ("Fork57" R !HasLeft75))) & WaitLeft38) | ((!WaitLeft89 | ("Fork57" R !HasLeft75)) & !WaitLeft38 & (WaitLeft89 | (!"Fork57" U HasLeft75)))
GWaitLeft16 & (!WaitRight8 | G!WaitLeft13)
F((!HasRight5 & (F!WaitLeft57 | FWaitRight13) & (GWaitLeft57 | G!WaitRight13)) | (HasRight5 & ((F!WaitLeft57 & FWaitRight13) | (GWaitLeft57 & G!WaitRight13))))
F(("Fork6" & !HasRight96) | (!"Fork6" & HasRight96)) | (!Idle4 U !WaitRight45)
FWaitRight95 & (FWaitLeft88 | FWaitLeft4)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment