update assignment (MTL property was wrong! i blame chatgpt)
This commit is contained in:
parent
e0863c9443
commit
a013fca768
1 changed files with 2 additions and 2 deletions
|
|
@ -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/#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>
|
||||
<p>Use <a href="https://deemz.org/public/teaching/mosis25/statebuddy/#eJx9Vu9r2zAQ/VeEP2wJpKmdpL/yYTDaUsa2rrQdDEoHqn1JxBwpk+Smacn+9t3ZlmPZTqEU9O690+ndSc5bwDOrzpWUENtganUGgxy6i7VK02A646lBaJVyaYlmgulbsRpmYmjV6hvM7HeVGbhQaxlMH4pgMAhasceBJ7wV88VeZSNYlz4pa9Vyv7oz3k6wt+6ucKP0Kvhzte/EGNl73pbKC713Vl/ZEX3nnF3aRrkmHmowYM8XWklVp9fhgpgIg8FNm+oHCnJKNf7wbHaQl+1eLKEjVw7XM81m7VSIFRSQyWUibJ3hoIIgZNwuewcWpCeYC9nMswMLEpryOeV6WedUWLXZHaR4u4SSjf12uMtG62t4sX6+Cq0yNn1yUNV+N1Q32DgDCXFNXBs2h9cFNAwd/Drcyn+LxfGuDapAJeHOqJzHnUVFsDbKzRI6Qg1ZV+HtSNderfK7Yh277dF5ITdG4N87Wj9uMbZQ66+wMe7RfVUK3YmolwY03soEOxxYanu5/zWnpuOdmAvLU7bmNl7QbOM4Kn1nuQV6m7XKpOVyngKmfngLMoFVBsfh8a6bRHsJppPweDg6GgSbYDqanAyPqCjxCmU0moyHJ0X0tAj+EZJScfy/xcNRaf4Wp0GBEmlmQbPIsEP22w1nc/+jI8ybbzAeh9vtoEoUhbtEh4fsfiEMwz+7AGYs11bIOVspIS1Tsxzlxoi5XAL2iNHtRBD5hiyJFygYMLFcpUAE0vI0zWWxkpa+cqA/GvYEC/4slEZnNfzNhM7pZtguOxyVZUcRGehVHnmVa6Vs2/ZT5+sYE3nqkae2IkbL5+0EpXx01tSPPf21soDn5DY/LHYhzRJI2EqrFQ7YhvWeQYvZhhwhQv6KsqcMB1nWLeiztUDDZlykTMkY2EZlmAQvVS7D2g50Tdrhl2tzMVJbGh6utVr703NCbx21txqP3Xiehtv8EXehqDQwH9uaA+FZI8kkqqY4OiPjvTyTk7Ac/yhv5CN9cfhSyYRKwxWOEd6tTbGQ6OyXi2B6HE3cq1y86e46lz+jEKxuNcE3heECPPTyBeKMuPeax+Dx6bJ76KqW4SG4Yr3GM84OPrHye9pHA5DQYnxgvV/sXwPt90nZu3oIB6MwDB9Zz2Xp9/P3iz9DkldS+sHxdM9QHghtCbf/AcDQckI=">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 & (X ~topRightPressed)) -> (G[0,2000] (lightOn)))</pre>
|
||||
<pre>G ((topRightPressed -> lightOn) & ((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>
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue