Help in evaluating TLA+ as a tool for a CRM application

[hornace...@gmail.com]

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

[Morgan Weetman]

Hi Martin,

As a bit of background, I'm a systems engineer working with open source software.

This is not a direct answer to your question, more a recommendation.

Your issue looks to be that the organisation has done something that *could* be done, but maybe *shouldn't* have been done.

I've done a little work in the past with Drools[1], which is specifically designed so that business users can easily modify business logic, rather than have developers do it.

There's an old proverb that goes something like "No matter how far you've gone down the wrong path, turn back.", and I think this applies to you. Rather than trying to write a test framework to manage the existing collection of plug-ins, I'd recommend that you invest your time in deploying a proper BRMS and integrating it with Dynamics.

I hope this helps,

cheers

[1] https://www.drools.org/

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/809a0575-f6da-4875-b35f-67bef473aafdn%40googlegroups.com.

[Calvin Loncaric]

I absolutely think TLA+ is applicable to your situation.

TLA+ is often presented as a tool for designing distributed systems---but what makes it great for designing distributed systems also makes it great for designing plugins:

• The system is composed of an environment and a program (e.g. the network and a cluster of servers, or in your case Dynamics 365 and your plugin)
• The environment drives events (e.g. packet delivery, or in your case the events that the plugin responds to)
• Testing the program is impractical because there is no easy way to exercise all the possible behaviors of the environment

...although, this shouldn't be news to you; it sounds like you've already guessed how TLA+ can help: "[...] 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".

In the best possible case, a TLA+ spec can serve as a precise design document that details what you believe to be true about the environment and lets you quickly evaluate possible changes to the plugin logic.

--

Calvin

[Morgan Weetman]

Hi Calvin,

I'm also a TLA+ beginner, just anticipating the next question... how would integration testing work? Martin mentioned that he had a lot of plug-ins, so would he have a 1:1 mapping of plug-in to spec, or one large spec including logic from all plug-ins?

It seems like there would be a state-space explosion with the second option, but then I can't see how the first option would test that one plug-in didn't affect the others.

many thanks

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABf5HMjXL9ohn71ydu5eWzucRWe%2BUBvuscDonQGeFvUDWeCJ1Q%40mail.gmail.com.

[hornace...@gmail.com]

Hi Morgan,

Thank you for the hint with the BRMS framework, I will check which tools are available and whether I could utilise them.

I am bit afraid how powerful those tools are, as the plug-in logic is quite complex, but let's see.

@Calvin: Good to hear that I am not completely barking up the wrong tree here :)

 I see Morgan's point though with the concern how to approach the system specification, i.e. one large spec vs or one spec per plug-in, but thinking about it I would say the solution would be somewhere in the middle.

 I can imagine grouping the plug-in business logic to non-overlapping "modules" and having one spec per "module".

The "integration testing" aspect is indeed what I (maybe due to lack of experience) cannot still envision.

Maybe I need to just study the existing specs and see if I will be able to come up with a sample spec that would model "my" system and go from there...

M.

Dátum: utorok 11. októbra 2022, čas: 6:33:40 UTC+2, odosielateľ: morgan....@gmail.com

[Calvin Loncaric]

You are both asking the hard questions. :)

Regarding how to decompose the system: I don't know enough specifics to tell you whether to make one big specification or many small ones. Instead, I'll say a few very general things that work well for me when I'm making that choice in my own work:

• Start with a correctness condition. Modeling any part of the system is wasted work unless you know what you'll be checking---and knowing what you'll be checking when you start will help identify what parts of the system are the most important.
• Start small. Once you have written down what it means for the system to be right, you want to get as quickly as possible to a point where you can start model checking and building confidence. Elaborating a small starting specification is much easier than building a big one from scratch. (I also recommend taking notes during this process. Often things I write down like "TBD: does the source code actually check this condition?" or "Note: these two variables can't be read together atomically" turn out to be real bugs later. But don't get bogged down yet trying to read every line of source code or split up every non-atomic sequence of steps.)
  
• Don't worry about state space explosion. Yes, it can be a real problem, but you will drive yourself insane if you try to worry about it from the outset. Get down a faithful specification first, and worry about the model checker second.

Regarding integration testing: this could mean many things, and I'm not sure I'm on the same page about what you're hoping for. I think this is a question about how to make sure all the different plugins work together correctly, in which case my advice is the same as above: start with one spec, but start small and build up.

--

Calvin

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8912c99e-4bf1-4bd9-a51c-bd66af265783n%40googlegroups.com.

[Marko Schuetz-Schmuck]

Since this hasn't been mentioned yet, I'll mention it: you can maybe use
refinement. You start with an overly abstracted specification and some
properties that you check with TLC, then refine some aspects of the
specification. You can specify the implementation relation between the
two levels of abstraction.

Best regards,

Marko

Calvin Loncaric <c.a.lo...@gmail.com> writes:

> You are both asking the hard questions. :)
>
> Regarding how to decompose the system: I don't know enough specifics to
> tell you whether to make one big specification or many small ones. Instead,
> I'll say a few very general things that work well for me when I'm making
> that choice in my own work:
>

> - Start with a correctness condition. Modeling any part of the system is

> wasted work unless you know what you'll be checking---and knowing what
> you'll be checking when you start will help identify what parts of the
> system are the most important.

> - Start small. Once you have written down what it means for the system

> to be right, you want to get as quickly as possible to a point where you
> can start model checking and building confidence. Elaborating a small
> starting specification is much easier than building a big one from scratch.
> (I also recommend taking notes during this process. Often things I write
> down like "TBD: does the source code actually check this condition?" or
> "Note: these two variables can't be read together atomically" turn out to
> be real bugs later. But don't get bogged down yet trying to read every line
> of source code or split up every non-atomic sequence of steps.)

> - Don't worry about state space explosion. Yes, it can be a real

> problem, but you will drive yourself insane if you try to worry about it
> from the outset. Get down a faithful specification first, and worry about
> the model checker second.
>
> Regarding integration testing: this could mean many things, and I'm not

> sure I'm on the same page about what you're hoping for. I *think* this is a

>>>> - The system is composed of an environment and a program (e.g. the

>>>> network and a cluster of servers, or in your case Dynamics 365 and your
>>>> plugin)

>>>> - The environment drives events (e.g. packet delivery, or in your

>>>> case the events that the plugin responds to)

>>>> - Testing the program is impractical because there is no easy way to

>>>>> - 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

>>>>> <https://groups.google.com/d/msgid/tlaplus/809a0575-f6da-4875-b35f-67bef473aafdn%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>>> .

>>>>>
>>>> --
>>>> You received this message because you are subscribed to the Google
>>>> Groups "tlaplus" group.
>>>> To unsubscribe from this group and stop receiving emails from it, send
>>>> an email to tlaplus+u...@googlegroups.com.
>>>>
>>> To view this discussion on the web visit

>>>> https://groups.google.com/d/msgid/tlaplus/CABf5HMjXL9ohn71ydu5eWzucRWe%2BUBvuscDonQGeFvUDWeCJ1Q%40mail.gmail.com
>>>> <https://groups.google.com/d/msgid/tlaplus/CABf5HMjXL9ohn71ydu5eWzucRWe%2BUBvuscDonQGeFvUDWeCJ1Q%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>>> .

>>>>
>>> --
>> You received this message because you are subscribed to the Google Groups
>> "tlaplus" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to tlaplus+u...@googlegroups.com.
>> To view this discussion on the web visit

>> https://groups.google.com/d/msgid/tlaplus/8912c99e-4bf1-4bd9-a51c-bd66af265783n%40googlegroups.com
>> <https://groups.google.com/d/msgid/tlaplus/8912c99e-4bf1-4bd9-a51c-bd66af265783n%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .

>>
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABf5HMgd5yDYtja9GfbcaXRCA1cbCA6bTX45x-Rx%3DaCHK1Mj3A%40mail.gmail.com.

--
Prof. Dr. Marko Schütz-Schmuck
Department of Computer Science and Engineering
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681

[Jeremy Wright]

Shameless self-promotion :-). 

I made a refinement walkthrough a few months ago:  

https://youtube.com/playlist?list=PLacslU3Fwm5sJx5fTcYgOt1oOj0JMKKc5

Following on Marko’s advice I came to enjoy refinement. I think of it as “…design your specification to be as simple as possible but no simpler…” well with refinement you can be simpler in order to express the correctness condition you care about. In my tutorial sortByMagic isn't useful other than to define the goal of my specification. Then incrementally define a more detailed system using refinement mapping to “keep you honest” on the way. 

Jeremy

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87mt9ytjji.fsf%40manjaro.mail-host-address-is-not-set.

--

Jeremy

[Marko Schuetz-Schmuck]

Dear Jeremy

Thanks a lot for sharing! I very much like the videos.

Best regards,

Marko

> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAC2JkJsBebkwfJF31Bk3Gr3SYXK4G%3DDmAQ-9YWdF%2BF5yE3CwRQ%40mail.gmail.com.

[anything...@gmail.com]

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.

[Martin Hornáček]

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 :)

ne 23. 10. 2022 o 7:11 anything...@gmail.com <anything...@gmail.com> napísal(a):

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/603e0050-ecd6-4416-b13a-2b7612d09631n%40googlegroups.com.

[Jeremy Wright]

You’re welcome. 

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAKbGFM%2Bk1bzrXH3UEkXaZ9sEjuH6JZZ5TNpCUw7v-L4ohPUXqA%40mail.gmail.com.

--

Jeremy