added SF => mardowk preview enhanced needed for the moment

SF/cours-1.md

@@ -0,0 +1,47 @@
+# SF - Cours 1
+
+Rappel des cours de SF:
+
+- Une formule LTL est une formule $\varphi$
+- soit la négation d'un formule
+- soit une formule $\land$ une autre formule
+- Le $X (next)$ d'une autre formule
+- le Finaly $(F)$ d'une formule
+- le Globaly $(G)$ d'une formule
+
+
+### Exercice
+
+vérifer que: t,i $\models$ F$\varphi$ ssi t,i $\models$ TU$\varphi$
+Définition: Il existe j$\geq$ i, t,i$\models \varphi$
+il existe j$\geq$i, t,j$\models\varphi$ et pour tout $i\leq k <j$ t, k $\models \top$
+
+vérifier que:
+$G\varphi\models\lnot F(\lnot \varphi)$
+
+### Exo 1
+a) G(trainGvoie => F($\lnot$ trainGvoie)) $\lor$ G(trianDvoie=>F($\lnot$ trainDvoie))
+A) G(trainDvoie $\lor$ trainGvoie => F($\lnot$trianDvoie $\land$ $\lnot$trianGvoie))
+
+b) GF(trainGvoie $\lor$ trianDvoie)
+
+
+c) G(trainGvoie $\land$ trainD => ($\lnot$trainDvoieU$\lnot$trianGvoie))
+
+### Exo 4
+a)
+1) vrai
+2) vrai
+3) faux
+4) vrai
+5) vrai
+
+
+### Exercice
+
+a) S(EXp): {[1:3], 5, 6}
+b) S(AXp): {3, 6}
+c) S(EFp): {TOUS}
+d) S(AFp): {TOUS !{1,4,8}}
+e) S(EqUr): {2, 3, 4, 5, 6}
+f) S(AqUr): {2, 3, 4, 5, 6}

SF/cours2.md

@@ -0,0 +1,23 @@
+# Réseaux de petri coloré
+graphe bi-partie, graphe à deux type de noeuds/arcs
+
+### Rapels
+réseau petri = quadruplet <P, T, W-, W+>
+
+Exercice durant cours.
+```mermaid
+graph TB
+0(a+b+c+e)-->1(b+c+d)
+0-->2(a+c+f+g)
+1-->3(b+c+i)
+2-->4(a+f+h)
+2-->5(a+c+e+g+i)
+4-->6(a+e+h+j)
+5-->6
+5-->7(c+d+g+i)
+6-->8(d+h+j)
+7-->9(c+g+i+j)
+7-->8
+8-->10(h+i+j)
+9-->10
+```

SF/cours3.md

@@ -0,0 +1,74 @@
+# Cours 3
+
+### diner philosophes
+
+0: <1 + 2, $\emptyset$, $\emptyset$, 1 + 2>
+1: <1, 2, $\emptyset$, 1>
+2: <1, $\emptyset$, 2, $\emptyset$>
+3: <$\emptyset$, 1 + 2, $\emptyset$, $\emptyset$>
+4: <2, 1, $\emptyset$, 2>
+
+Interblocage possible.
+
+**Q4:** pour résoudre le problème, prendre les 2 fourchettes en même temps.
+
+**Q5:**
+Prise des 2 fourchettes en même temps
+0: <1 + 2, $\emptyset$, 1 + 2>
+1: <2, 1, $\emptyset$>
+2: <1, 2, $\emptyset$>
+
+
+```mermaid
+graph LR
+0((pense))-->|p|1[prendre]
+1-->|p,f|2((Mange))
+2-->|p,f|3[rendre]
+3-->|p|0
+3-->|f + f++1|4((Fourchettes))
+4-->|f + f++1|1
+```
+
+### Problème du train et des segments
+
+```mermaid
+graph TB
+1((Libre))-->|s++1 + s++2|0[Passer]
+0-->|s++1, t|2((Occupé))
+2-->|s, t|0
+0-->|s + s++2|1
+```
+
+Etat du système: Couple <numtrain, num section
+
+0: < <1,1> + <4,2>, <2> + <3> + <5>>
+1: < <2,1> + <4,2>, <1> + <3> + <5>>
+2: < <2,1> + <5,2>, <2> + <3> + <4>>
+3: < <3,1> + <5,2>, <1> + <2> + <4>>
+...
+
+**Q2: propriétées**
+P1: le nombre de trains restent constants: Si toujours 2 trains dans l'état `occupé` alors toujours 2 trains dans le système. on ne résone pas sur les arcs, mais sur le graph de marquage.
+en pertry net:
+`query node (card(EtatSysteme) != 2)`
+
+P2: On a jamais 2 fois le même S dans les jetons.
+en petry net:
+`query node (card(EtatSysteme:(Field[0] == 1)) > 1 ...)`
+
+
+### Dépliage réseau de petri coloré
+
+```mermaid
+graph TB
+0((p1_1))-->8[t1_x11_x21]
+1((p1_2))-->9[t1_x12_x22]
+2((p2_1))-->8
+3((p2_2))-->9
+4((p3_1))
+5((p3_2))
+6((p3_3))
+7((p3_4))
+0-->10[t1_x1_x22]
+3-->10
+```

SF/cours6.md

@@ -0,0 +1,156 @@
+# Structure kripke
+
+### Exercice
+
+$M \vDash \Phi$
+
+$\Phi = FGc: \bot$
+$\Phi = GFc: \top$
+$\Phi = Ga: \bot$
+$\Phi = aU(G(b\lor c)): \top$
+$\Phi = X\lnot c \to XXc: \top$
+
+
+### automates de Büchi
+
+l'alphabet $\omega$ composé de ... est acceptant si il contient un nombre infinie de a, car l'automate lit un `a` pour sortir de 2 et aller dans 1, puis il reste dans 1 en lisant infiniement souvent 1.
+
+On ne regarde pas les traces qui ne sont pas acceptante, que celle acceptantes.
+
+**TEST:**
+L(A) = ${\omega \in {a, b}^\omega | |w|_b = \omega }$
+
+Réponse: $\Sigma^*.b^\omega$
+Une suite finis de a suivi d'une infinité de b ou notre alphabet complet suivit d'une suite infinie de b.
+
+### Exercice
+construire automat buchi pour: p, Xp.
+Lit: p
+```mermaid
+graph LR
+0((0))-->|Sigma_p|e((1))
+e-->|Sigma|e
+style 0 stroke:green
+style e stroke:red
+```
+
+Lit: Xp
+```mermaid
+graph LR
+0((0))-->|Sigma|1((1))
+1-->|Sigma_p|e((2))
+e-->|sigma|e
+style 0 stroke:green
+style e stroke:red
+```
+
+Lit: Fp
+```mermaid
+graph LR
+0((0))-->|Sigma|0
+0-->|Sigma_p|e((1))
+e-->|sigma|e
+style 0 stroke:green
+style e stroke:red
+```
+
+lit: XXp
+```mermaid
+graph LR
+0((0))-->|Sigma|1((1))
+1-->|Sigma|3((3))
+3-->|Sigma_p|e((2))
+e-->|sigma|e
+style 0 stroke:green
+style e stroke:red
+```
+
+Lit: Gp
+```mermaid
+graph LR
+0((0))-->|Sigma_p|0
+style 0 stroke:green
+style 0 stroke:red
+```
+
+Lit: FGp
+```mermaid
+graph LR
+0((0))-->|Sigma|0
+0-->|Sigma_p|e((2))
+e-->|Sigma_p|e
+style 0 stroke:green
+style e stroke:red
+```
+
+Lit: GFp
+```mermaid
+graph LR
+0((0))-->|Sigma|0
+0-->|Sigma_p|e((2))
+e-->|Sigma_p|e
+e-->|Sigma|0
+style 0 stroke:green
+style e stroke:red
+```
+
+Lit: pUq
+```mermaid
+graph LR
+0((0))-->|Sigma_p|0
+0-->|Sigma_q|e((1))
+e-->|sigma|e
+style 0 stroke:green
+style e stroke:red
+```
+
+Lit: pRq
+```mermaid
+graph LR
+0((0))-->|Sigma_q|0
+0-->|Sigma_p|e((1))
+e-->|sigma|e
+style 0 stroke:green
+style e stroke:red
+```
+
+### Exercice
+
+G(p-->Fq) ==> NNF
+
+$(false R ( \lnot p \lor (true  U q)))$
+
+lit aU(Xa)
+
+```mermaid
+graph LR
+0-->|a|0((0))
+0-->|Sigma|e((1))
+style 0 stroke:green
+style e stroke:red
+```
+
+```mermaid
+graph TB
+0["a U (Xa)"]-->1["a, X(a U Xa)"]
+0-->2["Xa"]
+1-->1
+2-->|Sigma|3[a]
+```
+
+```mermaid
+graph TB
+0["false R (!p || ( true U q))"]-->1["!p || true U q, X(!p || true U q)"]
+2-->0
+3-->4["true, X(tue U q)"]
+1-->3["true U q, X(true U q)"]
+3-->5["q"]
+1-->2["!p, X(!p || true U q)"]
+5-->0
+```
+
+```wavedrom {align="center"}
+{signal:
+    [{name: "P1", wave: "x...l...", data: ["P1"]},
+    {name: "P2", wave: "0...xxl.", date: ["P2"]}]}
+```