ENSEEIHT/projet-mini-genie-logiciel-systeme
1
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity

fin du rapport

Browse source
This commit is contained in:
Laureηt 2021-10-20 16:16:13 +02:00
parent 952f801e68
commit afe0660de8
No known key found for this signature in database
GPG key ID: D88C6B294FD40994
2 changed files with 32 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
rapport/rapport.pdf
View file

Binary file not shown.

32
rapport/rapport.tex
View file

@ -364,4 +364,36 @@ Pour transformer une WorkDefinition dasn un réseau de Petri, nous créons 4 pla
Pour transformer une WorkSequence, nous relions la place du predecesseur à la transition du successeur, par exemple dans le cas d'un linkType start2start nous relions un \_started à un \_start. Pour transformer une WorkSequence, nous relions la place du predecesseur à la transition du successeur, par exemple dans le cas d'un linkType start2start nous relions un \_started à un \_start.
Pour transformer une Resource, nous créons simplement un palce avec le bon nombre de tokens. Pour ce qui est des Requests d'une WorkDefinition nous relions le \_start et le \_finish de la WorkDefinition à la ressource avec les poids correspondants. Pour transformer une Resource, nous créons simplement un palce avec le bon nombre de tokens. Pour ce qui est des Requests d'une WorkDefinition nous relions le \_start et le \_finish de la WorkDefinition à la ressource avec les poids correspondants.
\newpage
\section{Logique Temporelle Linéaire (LTL)}
Dans l'optique d'une vérification de la terminaison et de la transformation correcte de notre modèle simplePDL en modèle petriNET, nous pouvons à partir du modèle simplePDL générer des propositions que nous demanderons par la suite à selte/tina de vérifier. \\
Pour vérifier la terminaison du processus, nous pouvons écrire:
\begin{textcode}
[] <> (WD1_finished /\ WD2_finished /\ WD3_finished);
\end{textcode}
Pour vérifier qu'une WorkDefinition ne soit que dans un seul état à la fois, nous pouvons écrire (via l'intermédiaire d'un xor):
\begin{textcode}
[] (((WD1_idle /\ -WD1_running /\ -WD1_finished)
\/ (-WD1_idle /\ WD1_running /\ -WD1_finished)
\/ (-WD1_idle /\ -WD1_running /\ WD1_finished))
/\ ((WD2_idle /\ -WD2_running /\ -WD2_finished)
\/ (-WD2_idle /\ WD2_running /\ -WD2_finished)
\/ (-WD2_idle /\ -WD2_running /\ WD2_finished))
/\ ((WD3_idle /\ -WD3_running /\ -WD3_finished)
\/ (-WD3_idle /\ WD3_running /\ -WD3_finished)
\/ (-WD3_idle /\ -WD3_running /\ WD3_finished)));
\end{textcode}
Pour vérifier qu'une WorkDefinition ne progresse que dans un seul sens, nous pouvons
\begin{textcode}
[] ((WD1_finished =>
[](-WD1_running /\ -WD1_idle /\ WD1_started))
/\ (WD2_finished => [](-WD2_running /\ -WD2_idle /\ WD2_started))
/\ (WD3_finished => [](-WD3_running /\ -WD3_idle /\ WD3_started)));
\end{textcode}
\end{document} \end{document}