surete append

surete/01_model_ascenseur.py

@@ -0,0 +1,69 @@
+from enum import Enum
+from dataclasses import dataclass
+
+class Etage(Enum):
+	A = 0
+	B = 1
+	C = 2
+
+@dataclass
+class Etat:
+	ascenseur: Etage = Etage.A
+	bouton_A: bool = False
+	bouton_B: bool = False
+	bouton_C: bool = False
+
+	def clone(self): return Etat(ascenseur=self.ascenseur, bouton_A=self.bouton_A, bouton_B=self.bouton_B, bouton_C=self.bouton_C)
+
+def transition(etat: Etat, bouton_A: bool, bouton_B: bool, bouton_C: bool):
+	if bouton_A: etat.bouton_A = True
+	if bouton_B: etat.bouton_B = True
+	if bouton_C: etat.bouton_C = True
+
+	if etat.bouton_A:
+		ascenseur = Etage.A
+		etat.bouton_A = False
+
+	elif etat.bouton_B:
+		ascenseur = Etage.B
+		etat.bouton_B = False
+
+	elif etat.bouton_C:
+		ascenseur = Etage.C
+		etat.bouton_C = False
+
+	return etat
+
+def tout_bool():
+	yield False
+	yield True
+
+def tout_etage():
+	yield Etage.A
+	yield Etage.B
+	yield Etage.C
+
+def tout_etat():
+	for etage in tout_etage():
+		for bouton_A in tout_bool():
+			for bouton_B in tout_bool():
+				for bouton_C in tout_bool():
+					yield Etat(ascenseur=etage, bouton_A=bouton_A, bouton_B=bouton_B, bouton_C=bouton_C)
+
+def tout_entree():
+		for bouton_A in tout_bool():
+			for bouton_B in tout_bool():
+				for bouton_C in tout_bool():
+					yield (bouton_A, bouton_B, bouton_C)
+
+set_ = set()
+for etat in tout_etat():
+	transition_map = {}
+	for entree in tout_entree():
+		res = transition(etat.clone(), *entree)
+		if str(res) not in transition_map: transition_map[str(res)] = []
+		set_.add(str(etat) + " + " + str(entree) + "\n=> " + str(transition(etat, *entree)))
+
+
+for line in set_:
+	print(line + "\n")

surete/01_model_checking.md

@@ -0,0 +1,58 @@
+- modèle : représentation mathématique
+- vérification : algorithme fournissant une preuve adaptée
+
+## modèle
+
+- système de transitions
+	- machine à état, avec des états non désirés
+
+- synchronicité
+	- synchrone
+		- opérations sur tous les circuits sont organisées par une seule horloge de manière granulaire
+		- physiquement, le temps de propagation des signaux est bien inférieur à la période de l'horloge
+
+	- asynchrone
+		- des signaux peuvent se propager entre circuits avant la fin d'un changement d'état d'un circuit
+		- comporte des signaux indépendants et des verroux de synchronisation
+		- exemple : échanges réseau, composants à plusieurs horloges 
+
+- transition
+	- synchrone : une transition change tous les circuits
+	- asynchrone : une transition ne concerne et change qu'un circuit
+
+### automate fini
+
+- ensemble d'état
+- ensemble de transitions
+- un 'langage' qui sert d'entrées système
+- une phrase qui est une entrée précise
+
+- les état finaux serviront de cas d'erreurs, nous cherchons donc à vérifier que l'état final ne peut pas être atteint
+
+- on peut différencier des langages pour analyser un sous ensemble de cas à vérifier lorsqu'on intègre de nouvelles entrées
+- faire le produit d'automates A et B, c'est former l'automate qui prends comme transition les tuples des entrées de A et B
+
+#### Exemple
+
+propriété : tout A est suivi d'un B dans le langage (b+ab)*
+
+
+### structure de kripke
+- défini par une liste de propositions
+- ensemble de variables propositionnelles (équation booléennes)
+- ensemble d'états
+- ensemble de transitions
+- pour chaque état, l'ensemble des propositions qui sont vérifiées par cet état
+
+#### traces
+- suite d'évènements / états
+
+- est un ensemble mathématique de la forme:
+	- toutes les suites avec :
+		- e_0 est un état de départ
+		- (e_n, e_n+1) est une transition existante
+
+- arborescence
+	- arbre des états possibles en arrivant à chaque état en partant de l'état initial
+		- racine : état de départ
+		- enfants d'un neud : états accessibles depuis cet état