Understanding Encapsulation in Alloy Modeling
Explore the concept of encapsulation in Alloy modeling, its benefits, and how to implement it effectively. Encapsulation allows for creating modular and maintainable models in Alloy, shielding users from internal implementations and enabling easy redesign without affecting other parts of the model.
Uploaded on Oct 11, 2024 | 0 Views
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Encapsulation in Alloy Roger L. Costello March 10, 2018
How to implement encapsulation in Alloy? The util/ordering module uses encapsulation: you call the module with a set and then you suddenly have all these functions available on the set: first, last, next, prev, etc. You are shielded from how the ordering module implemented those functions. That s encapsulation.
Benefits of encapsulation Use encapsulation when creating Alloy models. A benefit of encapsulation is that you can redesign an encapsulation module without impacting other parts of the model.
Heres how to implement encapsulation 1. Create a module. 2. Either have users pass in a set via a module parameter, or, create the set within the module. 3. Create an internal representation, using the private keyword. 4. Create operations (pred and fun) on the set. 5. Then, users operate on the set through the operations provided by the module.
Example that illustrates encapsulation in Alloy Create a module for the colors of a traffic light. The set of colors (red, yellow, green) are defined in the module and are public. The sequence in which the colors change (e.g., a red light changes to a yellow light which changes to a green light which changes back to a red light) is private. The module provides a function (fun) that users call to get the next color.
Here is a module that implements encapsulation module traffic_light_color privateonesig Color_Sequence { Next: Color -> Color } { Next = red -> yellow + yellow -> green + green -> red } fun next : Color -> Color { Color_Sequence.Next } abstractsig Color {} onesig red extends Color {} onesig yellow extends Color {} onesig green extends Color {}
Here is a sample use of the module open traffic_light_color open util/ordering[Time] sig Time {} sig Traffic_Light { color: Color one -> Time } { all t: Time - first | color.t = traffic_light_color/next[color.(t.prev)] } run {}
open traffic_light_color open util/ordering[Time] sig Time {} sig Traffic_Light { color: Color one -> Time } { all t: Time - first | color.t = traffic_light_color/next[color.(t.prev)] } run {} This qualifies next to indicate that we want the next relation in the traffic_light_color module, not the next relation in the ordering module.
