module GUI.LoadAllSERENE18 where

-- this file loads the files containing the code examples in the
-- SERENE18 paper of Stephan Adelsberger, Bashar Igried, Markus Moser,
--         Vadim Savenkov, and Anton Setzer
-- on
-- Formal Verification for Feature-based Composition of Workflows

-- Abstract
-- 1. Introduction
-- 2. Background and Context
-- 2.1. Software Product Lines
-- 2.2. Agda

open import demo.AgdaDemoSERENE

-- 3. Workflow Specification in FeatureAgda

open import GUI.GUIFeaturesPart8Paper

-- 4. Workflow Verification and Implementation
-- 4.1. State machines

open import GUI.GUIFeaturesPart2Paper

-- 4.2. Extending State Machines with Features

open import GUI.GUIFeaturesPart8MedicationPaper

-- 4.3. Calling Machines With Different Features in a Monadic Way

open import GUI.GUIFeaturesMonadicPaper
open import GUI.GUIFeaturesMonadicExamplePaper

-- 4.4. Case Studies Carried Out

-- Avanced example (Fig. 1)
-- 
open import GUI.GUIFeaturesMonadicExampleAdvancedPaper

-- Vending machine

open import GUI.GUIFeaturesPart8Paper
open import GUI.GUIFeaturesPart8CompiledVendingMachinePaper

-- Bankaccount

open import GUI.GUIExampleBankAccount

-- infinite Buttons

open import GUI.GUIExampleInfiniteBtnsAdvanced

-- 5. Related Work
-- 6. Conclusion
-- Bibliography