Dear Jeremy Thanks a lot for sharing! I very much like the videos. Best regards, Marko Jeremy Wright <jeremy@xxxxxxxxxxxx> writes: > 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 > > On Fri, Oct 14, 2022 at 11:41 AM 'Marko Schuetz-Schmuck' via tlaplus < > tlaplus@xxxxxxxxxxxxxxxx> wrote: > >> 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.loncaric@xxxxxxxxx> 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 >> > 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 >> >>>>> < >> 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...@xxxxxxxxxxxxxxxx. >> >>>> >> >>> 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+unsubscribe@xxxxxxxxxxxxxxxx. >> >> 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+unsubscribe@xxxxxxxxxxxxxxxx. >> > 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 >> >> -- >> 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/87mt9ytjji.fsf%40manjaro.mail-host-address-is-not-set >> . >> > -- > Jeremy > > -- > 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/CAC2JkJsBebkwfJF31Bk3Gr3SYXK4G%3DDmAQ-9YWdF%2BF5yE3CwRQ%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/871qr1ru1o.fsf%40manjaro.mail-host-address-is-not-set.
Attachment:
signature.asc
Description: PGP signature