Thanks for the hints, the refinement approach sounds reasonable. It seems a good place to start, especially for me with not that much experience with writing specs.
The top-down approach using refinement, i.e. start with initial state, then "a miracle occurs" and evaluate, should be a viable option in my case.
In general, I look at Dynamics 365 CE application as a system with many many possible states which can be described by the existence (or non-existence) of entity records and attribute values these entity records have. The user input (for example updating an attribute or creating a new record) are actions that the system allows.
The plug-in code, which is triggered by the user input, also consists of some actions, which eventually change the state of the system.
I see how I could use the spec to detect if a new plugin does not introduce (in some special cases) loops in the system. For example, an update of quote.discount attribute triggers a plugin to update parent opportunity.totalamount which in turn triggers a plugin that proportionally distributes the totalamount to all children quotes, hence updating the quote.discount. It would require a Pricing module which would be extended each time when a new plug-in should be introduced in the system.
The spec could grow to be quite long over time, but I don't see this as a big challenge. The state space explosion problem is still something I need to check.. I don't have yet a clear picture how I would approach logic where I'm dealing with numeric inputs. The numeric inputs are always bounded with some min and max values. So, in addition to specifying some calculation logic (like for example tax calculation), TLA+ could also help to identify possible cases which would result in an out of range class of errors.
I haven't mentioned yet that the plug-in code is not always executed synchronously. The system I am currently working with, most of the plug-in are executed synchronously. User input triggers the plugin and the user needs to wait for the plugin execution to finish. If the plugin logic results in an exception, the whole operation is rolled back. There is also another component as part of the Dynamics CRM platform, which are called workflows. Workflows are usually executed asynchronously and an example usage of these components is to implement some approval process for deals in the system.
I did not consider this when I raised the question, but as I am learning more about TLA+ and thinking about this topic it came to me as another area where TLA+ could help me to identify design issues before actual implementation.
Somehow, I am still not sure whether I am not just trying to use a hammer to drill a hole (just because I really like the hammer). It could be just a lack of experience on my part. But I am determined to find out.
@Jeremy: Thanks for sharing the videos, it helped :)
A couple of ideas for you regarding decomposition, this is pretty basic so I may well be telling you things you already know, but
1) or state based behaviour, if you consider moore machine type approach in particular then the states should be mutually exclusive, this is the first clue to where you might divide, but not the only one
2) Always look for modes to condition behaviour - I come from equipment background and example there is you can often condition underlying equipment behaviour with a mode in a seperate state machine of it's own
eg local/off/remote in a common case I work in - this can greatly reduce the state explosion
Finally however, interfaces can be difficult to manage, so at times you consider the balance of the complexity of the interface, vs the state explosion but also considering the value of encaspulation by splitting into two or more SM, which can greatly reduce your testing cases if you choose to architecturally manage the possibility of side effects in implemtation.
Hello everyone,
I am looking for some advice regarding TLA+, in particular in evaluating if could be the right tool for my problem. My experience with TLA+ is quite limited so I figured I'd ask people with more experience for advice.
On my current assignment, I am working with Dynamics 365 CE system. This system allows to develop a plug-in with custom business logic to modify or augment the standard behavior of the platform. Plug-ins are essentially handlers for events fired by Dynamics 365 Customer Engagement . You can subscribe, or register, a plug-in to a known set of events to have your code run when the event occurs.
For example, when user is creating an Opportunity entity record in the system, the system determines the Default Price List for the current user and sets this value on the newly created record.
Our implementation relies heavily on these customizations, i.e. there lot of plug-ins in the system with business logic that supports pricing and financing use cases, approval workflows, etc.
My main concern is mainly these points:
- Currently, we have no overview about the chain of events happening in the system. Imagine situations like a certain plug-in logic being fired twice resulting in wrong calculations as an end result, infinite loops, unnecessary wait times for some of the events etc.
- Testability of the system in general. The plug-in code is tested by unit test, but these won't test the behavior of the plug-in within the platform. We developed a set of Integration tests, that exercises the plug-in logic by invoking the events that should trigger the plug-in logic. From the example I've given above, the test will arrange a particular system state, send a Create request for Opportunity entity record and assert if the Price List value matches the expected Default Price List value hence verifying the system behavior.
- The plug-in code turned into a big ball of mud. The developers are afraid to touch some of the plug-in code with fear to introduce bugs when developing new features for critical business logic related to pricing or financing. The Integration tests I mentioned above provide a safety net, but they don't guarantee that in certain edge cases a bug hasn't slipped into the system.
What I strive for is to really gain confidence about the system behavior and avoid subtle bugs. From my perspective, the system could be viewed as black box where the events transform the system from one state to another. Ideally we would like to check that the state of the system after an event is "correct" as a result of the plug-in logic.
Does someone see a possibility that TLA+ could be a useful tool in this context? Maybe some tools which would support property-based testing would be more appropriate in this case, but I am still searching...
So far, I only experimented a bit with TLA+ as interesting pastime project. I found it both interesting and powerful, but it never occurred to me to use it as part of my current role as I simply thought that it is suited to solve problems in a completely different domain.
I wish a knew about it while is writing my diploma thesis on network coding for distributed storage systems though. It would save me some time.
Thank you for you opinions.
Martin
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/F_GZwpKW390/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/603e0050-ecd6-4416-b13a-2b7612d09631n%40googlegroups.com.