Here are some example AGREE models for teaching / learning the AGREE tool.
The models are in the 'models' directory, and documentation related to AGREE is in the 'documentation' directory.
The primary pedagogical model is the Microwave: the structure is provided, and you, the user, need to fill in the guarantees necessary to perform the proofs. The GPCA model is a large-scale model of an infusion pump, and the QFCS_V2 model is an example of a part of a quad-redundant flight control system developed by NASA and Sikorsky. The Toy_Example is a simple model demonstrating how compositional verification works, and how the choice of types for input/output ports can lead to different answers.
To run the models, one needs the OSATE environment, available here. Once OSATE is installed, follow the directions in the documentation/AGREE/Agree Users Guide.