Re: [tlaplus] Help in evaluating TLA+ as a tool for a CRM application

[Calvin Loncaric <c.a.loncaric@xxxxxxxxx>]

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

On Tue, Oct 11, 2022 at 10:40 AM hornace...@xxxxxxxxx <hornacek.martin@xxxxxxxxx> wrote:

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....@xxxxxxxxx

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

On Tue, Oct 11, 2022 at 9:49 AM Calvin Loncaric <c.a.lo...@xxxxxxxxx> wrote:

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

On Sun, Oct 9, 2022 at 11:01 AM hornace...@xxxxxxxxx <hornace...@xxxxxxxxx> wrote:

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 the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/809a0575-f6da-4875-b35f-67bef473aafdn%40googlegroups.com.

--
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...@xxxxxxxxxxxxxxxx.

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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8912c99e-4bf1-4bd9-a51c-bd66af265783n%40googlegroups.com.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABf5HMgd5yDYtja9GfbcaXRCA1cbCA6bTX45x-Rx%3DaCHK1Mj3A%40mail.gmail.com.