Specifying Monitored Functions (using Signature plugin)
From CoreASM Wiki
We would like a way to specify monitored functions using our signature plugin. We discussed various approaches:
Proposals
- One possible approach could be to specify the source for monitored function values in the signature. For example we can have a monitored function readFromMyFile that actually reads values from the plugin-defined monitored function readFromFile("file://myfile.txt").
- We think that in the above case we in fact have a derived function not a monitored function (which can be defined in any fashion we define our derived functions). Thus, we see the following forms of monitored functions:
- Monitored functions defined by plugins: these functions do not need a signature in CoreASM specifications.
- Monitored functions defined by users (in specifications): for these functions, we need a way to assign values. We can do the following:
- If the range of the defined monitored function is enumerable, the engine can randomly choose a value and return that value (such value will be static for each state).
- If that is not possible, the engine should/can ask the value of the function the moment it is first needed.
Discussion
Objection: the random choice of value for monitored functions with enumerable range is quite inconvenient for simulation purposes. As the non-deterministic choice of an element from an enumerable background can be expressed easily with choice, it is probably more expedient to always ask the user (via the general input mechanism, that will provide redirection and plumbing sooner or later), unless the specifier has defined the monitored function as a derived function.
There is an opportunity here to introduce, as notationally convenient, a choose-expression, e.g. any enumerable — maybe with an optional with clause to select specific elements. We would then have
any E = return x in choose t in E do x:=t
(assuming we don't already have a choose-expression!) and similarly for the version with with predicate.
