research/statebuddy
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

assignment: fix property (it was wrong) + always include traces for 'true' and 'false'

Browse source
This commit is contained in:
Joeri Exelmans 2025-11-07 15:09:21 +01:00
parent fcf9448441
commit 2dd35ab079
2 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
assignment.html
View file

@ -317,12 +317,12 @@ The controller can send the following events to the plant:
<h2>Starting point</h2>
<p>Use <a href="https://deemz.org/public/teaching/mosis25/statebuddy/#eJx9Vm1v2jAQ/itWPmwgUZoAfePDpKntpmlbV/XlE2KSSQ6wFmxmO1Basd++u7wRJ6FSVcnP89zj893Z4c3jiVXXSkoIrTe2OoFeCj2GWsWxN57z2CC0jrm0JDPe+C1b9RPRt2r9A+b2p0oM3Kit9MaTjPR6XoOb9pzAB7FYHo2skdXQmbJWrY5Ht/JNg6N5t9G11EvyeX3sxMgcPW8jyqHeO6sb2cK+c8622Fq6JuxrMGCvl1pJVZVX4UwYCYPkril1iUwcU46/nDIXkOP2JFbQ4pXCVaf5vGmFWCYBGd1GwlYVBZQJhAybaR/ATDSDhZB1nwOYibAon2OuV1VNiZWbPUKMt0soWdvvgBdutL6DF+v6lWjpWK9TAZXtL4bqHhtnICKtCSvDVuDVABqGFn0Vbvg/YHK8bYOSKEN4UahUx4sSZWRllOsptFC1sLbEm0zbXo3027iW3Y7EOVQxRuDeO1pP98gt1fY77Ezx6L4qhdUJqJcGNN7KCDvsWWp7vv8dp6bjnVgIy2O25TZc0mzjOCr9aLkFepu1SqTlchEDWk/evERglt65f37oJslevPHIP+8PznrezhsPRhf9M0pKvELOBqNh/yJjLzPyj5BkxfH/Hg9HqblbXHoZSqK5Bc0Cw07Z72I46/ufnaFvusFw6O/3vdIo8A9Gp6fsaSkMwz+7BGYs11bIBVsrIS1T8xTlxoiFXAH2iNHtRBD1hkoSLjGgx8RqHQMJKJbHcRoWKmnpKwf6o2EzWPKNUBorq+FvInQqN/1m2v4gTzsIqIBO5oGTuVbKNst+WdR1iEZO9MCJtiLEki+aBnn44KoeP3Ti75QFPCe36WGxC3ESQcTWWq1xwHasswEt5juqCAnSV5TNEhxkWS1Bl20FFmzORcyUDIHtVIImeKnSMMztRFdCW+pVtDkbqT0ND9dabd3puaC3jtpbjsdhPC/9ffqIF1SQFzAd20oF/KuaySgopzi4osI7PqMLPx//IG3klL44fKVkRKnhCscI79YuW0is7Lcbb3wejIpXOXvTi+uc/4xCsLzVBN9nBRfgoLcvECakfdI8BEdPl91B1xWHifeVdWrPODv5xDr5B5U9s86/Ov+BfZn4vcGU5aJut5u+T3wDUbpTfl6O2W8gTxiP7e//A16saTI=">this link to the starting point</a> for this assignment.</p>
<p>Use <a href="https://deemz.org/public/teaching/mosis25/statebuddy/#eJx9Vm1r2zAQ/ivCH7YE0tTOW9t8GIy2lLGtK20Hg9KBYl8SMUfKJDlpWrLfvju/xbKdQinoeZ57dLo7yXnzeGLVpZISQutNrU6gl0IPoVZx7E3nPDYIrWMuLcmMN33LVv1E9K1af4O5/a4SA1dqK73pU0Z6Pa/BPfecwHuxWB6NrJHV0JmyVq2OR7fyTYOjebfRtdRL8uf62ImROXreRpRDvXdWN7KFfeecbbG1dE3Y12DAXi61kqoqr8KZMBIGyV1T6hKZOKYcfzhlLiDH7VGsoMUrhatO83nTCrFMAjK6joStKgooEwgZNtM+gJloBgsh6z4HMBNhUT7HXK+qmhIrN3uAGG+XULK23wEv3Gh9Cy/W9SvR0rFepwIq218M1R02zkBEWhNWhq3AqwE0DC36Ktzwv8fkeNsGJVGG8KJQqY4XJcrIyijXU2ihamFtiTeZtr0a6bdxLbsdiXOoYozAvXe0ft4jt1Tbr7AzxaP7qhRWJ6BeGtB4KyPssGep7fn+t5yajndiISyP2ZbbcEmzjeOo9IPlFuht1iqRlstFDGj99OYlArP0Jv7k0E2SvXjTkT/pD8Y9b+dNB6Oz/piSEq+Qs8Fo2D/L2POM/CMkWXH8v8fDUWruFudehpJobkGzwLBT9rsYzvr+4zH6phsMh/5+3yuNAv9gdHrKHpfCMPyzS2DGcm2FXLC1EtIyNU9RboxYyBVgjxjdTgRRb6gk4RIDekys1jGQgGJ5HKdhoZKWvnKgPxo2gyXfCKWxshr+JkKnctNvpu0P8rSDgAroZB44mWulbLPs50Vdh2jkRA+caCtCLPmiaZCHDy7q8UMn/lZZwHNymx4WuxAnEURsrdUaB2zHOhvQYr6jipAgfUXZLMFBltUSdNlWYMHmXMRMyRDYTiVogpcqDcPcTnQltKVeRZuzkdrT8HCt1dadnjN666i95XgcxvPc36ePeEEFeQHTsa1UwL+omYyCcoqDCyq84zM68/PxD9JGPtMXh6+UjCg1XOEY4d3aZQuJlf1y5U0nwah4lbM3vbjO+c8oBMtbTfBdVnABDnr9AmFC2kfNQ3D0dNkddF1xePJuWKdTe8fZB9b5xf7V0G6XnXxinZsnvzfwff+ZdfKPbrfbTZ8nvoEo3Sg/LsfkN5Dni6f29/8Bmvhncw==">this link to the starting point</a> for this assignment.</p>
<h2>Testing your solution</h2>
<p>To test your solution, initialize the execution, and interact with the plant UI. The execution can run in (scaled) real-time, with the ability to pause/resume.</p>
<p>To gain more confidence that you correctly implemented the requirements, you can write Metric Temporal Logic (MTL) properties. An example of such a property is:
<pre>G (topRightPressed -> (lightOn U (~topRightPressed & F[0,2] lightOn)))</pre>
<pre>G ((topRightPressed & (X ~topRightPressed)) -> (G[0,2000] (lightOn)))</pre>
meaning: "as long as the top-right button is pressed, the light should be on, and after the top-right button is released, the light should remain on for 2 seconds" AKA Requirement 1.
</p>

5
src/App/check_property.ts
View file

@ -36,7 +36,10 @@ export async function checkProperty(plant: Plant<RT_Statechart, any>, property:
return [entry];
}, [] as {simtime: number, state: any}[]);
let traces = {} as {[key: string]: [number, any][]};
let traces = {
'true': [0, true] as [number, any],
'false': [0, false] as [number, any],
} as {[key: string]: [number, any][]};
for (const {simtime, state} of cleanPlantStates) {
for (const [key, value] of Object.entries(state)) {
// just append