feat: a LOT of stuff (final report, examples, simulation of a single assert, move from node instances to node definitions, etc.)

doc/data/middle.csv

@@ -0,0 +1,101 @@
+0.1,1.,1.
+0.2,1.09,0.9
+0.3,1.1606355,0.706355
+0.4,1.20740674526,0.467712452587
+0.5,1.23139725894,0.23990513678
+0.6,1.23688017859,0.0548291965681
+0.7,1.22854167208,-0.0833850651095
+0.8,1.21004121057,-0.185004615107
+0.9,1.18373429159,-0.263069189855
+1.,1.15086755111,-0.328667404789
+1.1,1.1118247,-0.390428511056
+1.2,1.06627366782,-0.455510321832
+1.3,1.01317876753,-0.530949002857
+1.4,0.950656415679,-0.625223518541
+1.5,0.875618537104,-0.750378785745
+1.6,0.783071598116,-0.925469389886
+1.7,0.664795417332,-1.18276180784
+1.8,0.506869445305,-1.57925972026
+1.9,0.285198697436,-2.21670747869
+2.,-0.0411442507765,-3.26342948213
+2.1,-0.529971005861,-4.88826755084
+2.2,-1.18926322222,-6.59292216359
+2.3,-1.70007492651,-5.10811704286
+2.4,-1.71110375487,-0.110288283653
+2.5,-1.6943904386,0.167133162707
+2.6,-1.67636818234,0.180222562559
+2.7,-1.65789428106,0.184739012827
+2.8,-1.63899329307,0.189009879909
+2.9,-1.61963873086,0.193545622084
+3.,-1.59979623066,0.19842500202
+3.1,-1.57942644945,0.203697812082
+3.2,-1.5584846181,0.20941831349
+3.3,-1.53691956293,0.215650551743
+3.4,-1.5146724274,0.222471355336
+3.5,-1.4916750512,0.229973761947
+3.6,-1.46784790356,0.2382714764
+3.7,-1.44309742078,0.247504827798
+3.8,-1.41731253591,0.257848848732
+3.9,-1.39036009703,0.269524388767
+4.,-1.36207873371,0.282813633255
+4.1,-1.3322705209,0.298082128026
+4.2,-1.30068946176,0.315810591386
+4.3,-1.26702528703,0.336641747347
+4.4,-1.23088021532,0.361450717085
+4.5,-1.1917348921,0.391453232213
+4.6,-1.14889727973,0.428376123701
+4.7,-1.10142396201,0.474733177166
+4.8,-1.04799551139,0.534284506253
+4.9,-0.986712969524,0.612825418644
+5.,-0.914754444531,0.719585249924
+5.1,-0.827775684935,0.869787595966
+5.2,-0.718829259023,1.08946425911
+5.3,-0.576368481233,1.42460777791
+5.4,-0.380576409527,1.95792071706
+5.5,-0.0972616434138,2.83314766113
+5.6,0.327343067813,4.24604711227
+5.7,0.938227766901,6.10884699088
+5.8,1.57630039075,6.38072623847
+5.9,1.72492948547,1.48629094717
+6.,1.70950968622,-0.1541979925
+6.1,1.6918164813,-0.176932049138
+6.2,1.67367963513,-0.18136846171
+6.3,1.6551400682,-0.185395669303
+6.4,1.63617378367,-0.189662845297
+6.5,1.61674960397,-0.194241796996
+6.6,1.59683206882,-0.199175351464
+6.7,1.57638103454,-0.204510342852
+6.8,1.55535084938,-0.210301851627
+6.9,1.53368929463,-0.216615547499
+7.,1.51133625499,-0.223530396355
+7.1,1.48822203852,-0.231142164754
+7.2,1.46426523263,-0.239568058841
+7.3,1.43936993788,-0.248952947563
+7.4,1.41342215567,-0.259477822069
+7.5,1.38628500991,-0.271371457617
+7.6,1.35779233631,-0.28492673593
+7.7,1.32773994949,-0.300523868279
+7.8,1.29587354655,-0.318664029389
+7.9,1.26187164466,-0.34001901883
+8.,1.22532103041,-0.365506142586
+8.1,1.18568065733,-0.396403730709
+8.2,1.14222727487,-0.434533824692
+8.3,1.09397137632,-0.482558985489
+8.4,1.03952350195,-0.544478743691
+8.5,0.976874889936,-0.626486120115
+8.6,0.903025524298,-0.738493656375
+8.7,0.813331641428,-0.896938828698
+8.8,0.700324127342,-1.13007514087
+8.9,0.551522102003,-1.48802025338
+9.,0.345434892204,-2.060872098
+9.1,0.0451454340179,-3.00289458186
+9.2,-0.405434196095,-4.50579630113
+9.3,-1.04021686075,-6.34782664655
+9.4,-1.63855504333,-5.9833818258
+9.5,-1.7164488535,-0.778938101736
+9.6,-1.70137983829,0.150690152195
+9.7,-1.68357260618,0.178072321076
+9.8,-1.66526259017,0.183100160094
+9.9,-1.64653268832,0.187299018484
+10.,-1.62736154517,0.191711431492
+

doc/remarques.typ

@@ -1,3 +1,7 @@
+#set par(justify: true)
+
+= Version 1.
+
 La phrase "it is less computationally intensive... the compiler". est mal dite;
 tu peux dire que c'est la methode classique, par exemple, implementee pour
 simulink et aussi Zelus.
@@ -224,5 +228,121 @@ phases d'integration (le temps ronronne) et des pas discrets (reactions
 instantanees).
 
 Super. Continue ! --Marc
+#pagebreak()
+
+= Version 2.
+
+*L.230 - 235*. Le discours peut donner l'impression de confondre simuation et
+  modèle  mathématique. Tu écris un modèle mathématique idéalisé, c.à.d. avec un
+  choc élastique où la vitesse change instantanément de direction. Pour cela, la
+  manière de simuler doit changer. La, tu peux garder le discours.
+
+"_Since time is logical in discrete nodes_". Tu veux dire plutôt que l'on
+choisit de décrire des réactions en temps zéro (ou instantanées), c'est bien
+ça ? "_Since time is logical in discrete nodes, nothing tells us when, in
+continuous time, we should perform discrete steps._" Je ne comprends pas cette
+phrase !
+
+*L. 242-245*. Si tu veux définir le zéro-crossing, ne faudrait-il pas plutôt le
+faire avec une définition d'analyse d'abord et décrire ensuite, si besoin
+l'algorithme (mais informellement) ? L'intuition, c'est qu'il y a un
+zéro-crossing de $z$ en $t_0$, entre $t_"left"$ et $t_"right"$ lorsque il existe
+une boule d'épaisseur non nulle autour de $t_0$ (d'épaisseur $epsilon$) telle
+que pour tous les points a gauche de t0 (notons
+$t_0^- = { t | t <= t_0 and |t_0 - t| <= epsilon }$), $z(t_0^-) <= 0$ et tous
+les points a droite, $z(t_0^+) > 0$. Tim t'as donné l'article qui décrit l'algo.
+Illinois. Je ne l'ai pas sur moi. Le signal $z: [t_"left", t_"right"]$ a un
+zéro-crossing en t0 lorsque il existe un $epsilon > 0$ tq pour tout
+$alpha < epsilon$: ... . Qu'en penses-tu ?
+
+*Listing 5*. Tu n'expliques pas `last y'`.
 
 
+*P.10*. Tu devrais d'abord expliquer le modele mathématique, ce dont tu as
+besoin, puis l'exemple; ou bien l'inverse, expliquer d'abord intuitivement
+l'exemple, les ingrédients dont tu as besoin et que tu introduits, plus le
+modèle mathématique. Et ensuite, les choses dont tu as besoin pour simuler.
+E.g., connaitre $f_"der"$, $f_"zero"$, l'état initial continu, l'état discret,
+etc.
+
+*L.302*.
+Je trouve l'écriture $h in [0, v.h]$ un peu troublante. Est-ce qu'une notation
+$v\#h$ ou autre ne serait pas mieux ? Ou alors, utiliser plutôt un champ
+"horizon" que h, dans la notation en point. Ou "right" ?
+
+"_Multiple methods exist (Zélus uses the Illinois method [Sny53])_". La méthode
+Illinois est la plus connue et utilisée. C'est mal formulé. Multiple methods
+exist; one of the oldest and most-used method is the Illinois method. It is
+used, for example, in the Sundials CVODE suite (donner la référence; regarde
+le manuel). Simulink also used this method by default. Zelus also implements
+this method.
+
+*L.305-309*.
+C'est un peu confus. Dis simplement ce que fait une méthode de zéro-crossing et
+des ingrédients dont elle a besoin, avant d'expliquer, plus tard, comment on
+s'en sert dans la simulation.
+Tu as besoin de $g: T i m e -> X -> Z_o$; de $x_0: X$; de $t_"left"$, de
+$t_"right"$ et de $d e n s e: T i m e -> X$, défini sur cet intervalle. La
+fonction de zéro-crossing indique qui, sur le vecteur $Z_o$, traverse zéro. Tu
+peux signaler les difficultés éventuelles (on peut rater un événement, c'est
+sensible a la largeur de l'intervalle de détection, au fait que le nombre de
+traversées peut être paire et on rate l'événement, etc.). Et dire que on ne fait
+rien là dessus (pas plus que Simulink, Modelica, et les autres d'ailleurs).
+
+*L. 322-324*. Je ne comprends pas la définition entre la ligne 322 et 324 et pas
+bien le paragraphe précédent.
+
+*L. 418*. Tu veux plutôt dire que tu voudrais pouvoir agréger les solutions
+denses successives ($d k y$). Les solveurs classiques sont impératifs,
+c'est-à-dire qu'ils ont un état interne et que chaque appel à "step" le modifie
+physiquement. Pour pouvoir agréger plusieurs solutions successives, il faut
+qu'il fournisse un moyen de le faire. (Rmq: ce n'est pas forcément une "copie
+d'état" dont on a besoin. Pour RK, je l'ai fait en fournissant un moyen d'avoir
+une copie de $d k y$. Ça suffit.)
+
+*L. 459*. Si tu parles d'assertions dans les programmes, cite/lis les articles
+classiques car c'est une construction très ancienne des langages de
+programmation. Je ne suis pas spécialiste mais j'en ai lu deux vieux (de
+mémoire, un de Hoare; un de Dijsktra). Je suis sûr qu'il doit y avoir un article
+de survey que tout le monde cite la dessus. Je regarderai en rentrant. En somme,
+dis aussi pourquoi c'est intéressant/utile de pouvoir écrire des assertions et
+les difficultés que cela pose dans le cas présent.
+
+"_An important property of assertions is that they are transparent: their
+presence does not affect the result of the computation._" An expected feature of
+run-time assertions is that they should not affect the rest of the computation
+(except stopping execution when they are not fulfilled). We call them
+"transparent", in the sense that, running the program with or without, if no
+error is raised, should produce the same result.
+
+*Figure 9*. Je ne comprends pas la figure 9. Tu veux dire que, en Lustre, cela
+correspond à avoir un seul noeud qui calcule les deux en parallèle ? On n'écrira
+jamais le code de la partie droite. Relis l'article sur les assertions de Lustre
+(de memoire, AMAST 93). En Lustre, les assertions ont un role qui consiste à
+contraindre l'environnement, avant tout. C'est utile quand on veut vérifier des
+propriétes. En fait, une assertion se decompose en deux parties, une hypothèse
+(qui parle des entrées, incontrolâbles), et une conclusion (assume/guarantee).
+Dans notre cas, comme on veut s'en servir d'abord comme on le fait dans un
+langage généraliste et, pour le moment, pas pour faire de la vérification, on ne
+distingue pas les deux. Le programme de gauche est equivalent à
+```
+let node f (x) =
+ let v = ... in
+ let assertion = (let p = integr(0.0, v) in p >= 0.0) in
+ (v, assertion)
+```
+c.à.d. que assertion est un flot comme les autres. Est-ce autre chose que cela
+que tu veux dire ?
+
+*L. 477*.
+Pas vraiment. Un noeud Lustre avec une assertion a vérifier dynamiquement,
+s'implémente en calculant un flot supplementaire et en vérifiant qu'il est vrai
+à chaque instant. On le calcule donc avec le reste du code, comme on le fait
+habituellement pour les assertions dans les langages classiques. Attention: je
+ne parle pas ici de vérification formelle. On traite de manière particulière les
+assertions quand on cherche a vérifier une propriété. En Lustre, on considère
+que les assertions sont vraies et on vérifie qu'elles ne dépendent pas des
+sorties; sinon, elle ne sont pas causales. C'est pour cela, qu'il faut
+distinguer les hypothèses (assume) des résultats attendus (guarantee).
+
+Il n'y a aucun exemple ?

doc/sources.bib

@@ -212,3 +212,91 @@
 	volume = {4},
 	year = {1953},
 }
+@article{cit:assertion_hist,
+	title = {A historical perspective on runtime assertion checking in software
+	         development},
+	volume = {31},
+	ISSN = {0163-5948},
+	DOI = {10.1145/1127878.1127900},
+	abstractNote = {This report presents initial results in the area of software
+	                testing and analysis produced as part of the Software
+	                Engineering Impact Project. The report describes the
+	                historical development of runtime assertion checking,
+	                including a description of the origins of and significant
+	                features associated with assertion checking mechanisms, and
+	                initial findings about current industrial use. A future
+	                report will provide a more comprehensive assessment of
+	                development practice, for which we invite readers of this
+	                report to contribute information.},
+	number = {3},
+	journal = {ACM SIGSOFT Software Engineering Notes},
+	author = {Clarke, Lori A. and Rosenblum, David S.},
+	year = {2006},
+	month = may,
+	pages = {25–37},
+	language = {en},
+}
+@article{cit:assertion_axiom,
+	title = {An axiomatic basis for computer programming},
+	volume = {12},
+	ISSN = {0001-0782},
+	DOI = {10.1145/363235.363259},
+	abstractNote = {In this paper an attempt is made to explore the logical
+	                foundations of computer programming by use of techniques
+	                which were first applied in the study of geometry and have
+	                later been extended to other branches of mathematics. This
+	                involves the elucidation of sets of axioms and rules of
+	                inference which can be used in proofs of the properties of
+	                computer programs. Examples are given of such axioms and
+	                rules, and a formal proof of a simple theorem is displayed.
+	                Finally, it is argued that important advantage, both
+	                theoretical and practical, may follow from a pursuance of
+	                these topics.},
+	number = {10},
+	journal = {Commun. ACM},
+	author = {Hoare, C. A. R.},
+	year = {1969},
+	month = oct,
+	pages = {576–580},
+}
+@article{cit:assertion_lustre,
+	title = {Programming and verifying real-time systems by means of the
+	         synchronous data-flow language LUSTRE},
+	volume = {18},
+	rights = {
+	          https://ieeexplore.ieee.org/Xplorehelp/downloads/license-information/IEEE.html
+	          },
+	ISSN = {00985589},
+	DOI = {10.1109/32.159839},
+	number = {9},
+	journal = {IEEE Transactions on Software Engineering},
+	author = {Halbwachs, N. and Lagnier, F. and Ratel, C.},
+	year = {1992},
+	month = sep,
+	pages = {785–793},
+}
+@inbook{cit:hyb_auto,
+	address = {Berlin, Heidelberg},
+	title = {The Theory of Hybrid Automata},
+	ISBN = {978-3-642-59615-5},
+	url = {https://doi.org/10.1007/978-3-642-59615-5_13},
+	DOI = {10.1007/978-3-642-59615-5_13},
+	abstractNote = {A hybrid automaton is a formal model for a mixed
+	                discrete-continuous System. W e classify hybrid automata
+	                acoording to what questions about their behavior can be
+	                answered algorithmically. The Classification reveals
+	                structure on mixed discrete-continuous State Spaces that was
+	                previously studied on purely discrete state Spaces only. In
+	                particular, various classes of hybrid automata induce
+	                finitary trace equivalence (or similarity, or bisimilarity)
+	                relations on an uncountable State space, thus permitting the
+	                application of various model-checking techniques that were
+	                originally developed for finitestate Systems.},
+	booktitle = {Verification of Digital and Hybrid Systems},
+	publisher = {Springer},
+	author = {Henzinger, Thomas A.},
+	editor = {Inan, M. Kemal and Kurshan, Robert P.},
+	year = {2000},
+	pages = {265–292},
+	language = {en},
+}