[PATCH] glossary: Add terms

[Sebastian Huber]

On 29.11.23 09:13, Sebastian Huber wrote:
> On 28.11.23 20:49, Andrew.Butterfield at scss.tcd.ie wrote:
>>     +    scenario
>>     +        In a setting that involves many concurrent tasks that
>>     interleave in arbitrary
>>     +        ways, a scenario describes a single specific possible
>>     interleaving.  One
>>     +        interpretation of the behaviour of a concurrent system is
>>     the set of all its
>>     +        scenarios.
>>     +
>>
>> This doesn't cover the common use case of a test scenario which is 
>> usually
>>
>> less about threading and more about values and using a set of methods in
>>
>> a particular manner.
>>
>> In the context in which Sebastian asked me for this entry, the term 
>> `scenario` is used as described above.
>>
>> But you are right that there are nuances here. In the Promela/SPIN 
>> based test-generation work, each
>> counter example we get from SPIN describes a scenario as defined 
>> above, and we generate C test code
>> that reproduces that scenario, including the precise interleaving of 
>> the tasks as per  that scenario.
> 
> The term scenario is used a lot in the formal verification chapter, so 
> it should have an entry. Joel, do you have a suggestion to improve the 
> wording?

I added an "In the context of formal verification, ..." to the term 
definition and checked it in.

-- 
embedded brains GmbH & Co. KG
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.huber at embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/