xekoukou

module Magda where

--We need to model the agents that interact with the software.
-- , the world.
-- Each agent has specific material properties that make him better suited in specific computations
-- and specific material jobs. Thus agents need to have as type , a specific role of a system.

-- Roles have meaning inside specific organizational structures. or in other words the type of work performed and
-- the type of computation determines the roles that are needed, in a way that not one role can be taken apart and analyzed independently.

xekoukou

open import Prelude.Nat
open import Prelude.Equality
open import Prelude.Product
open import Prelude.Unit
open import Prelude.Show
open import Prelude.Bool
open import Prelude.String
open import Prelude.Semiring
open import Prelude.Equality

xekoukou

open import Prelude.Nat
open import Prelude.Equality
open import Prelude.Product
open import Prelude.Unit
open import Prelude.Show
open import Prelude.String
open import Prelude.Semiring

xekoukou

open import Prelude.Nat
open import Prelude.Equality
open import Prelude.Product
open import Prelude.Unit
open import Prelude.Show
open import Prelude.String
open import Prelude.Semiring

xekoukou

open import Data.Nat as ℕ
open import Data.Fin hiding (inject≤)
open import Relation.Binary.PropositionalEquality



inject≤ : ∀ {m n} → Fin m → m ℕ.≤ n → Fin n
inject≤ {_} {suc n} zero    le = zero
inject≤ {_} {suc n} (suc i) le = suc (inject≤ i (ℕ.≤-pred le))

xekoukou

import Relation.Binary.PropositionalEquality as P
open import Data.List using (List ; [] ; _∷_ ; tabulate ; lookup ; filter)
open import Relation.Nullary
import Function as F




e : ∀{ℓ} → {A : Set ℓ} → (∀ (x y : A) → Dec (x P.≡ y)) → List A → List A

xekoukou

 ------------------------------ MODULE Blinkers ------------------------------

EXTENDS Integers

VARIABLES x , y
          

Init1 == x   = 1
Init2 == y   = 1 

xekoukou

open import Data.Nat
open import Data.Fin hiding (_+_)
open import Data.Product
import Relation.Binary.HeterogeneousEquality as H

Types : Set₁
Types = ℕ → Set

Seq : Types → Set
Seq t = (n : ℕ) → t n

xekoukou

-- `accepts`, in defunctionalized style:
accepts :: State -> String -> Bool
accepts S0 ('a':xs) = accepts S1 xs
accepts S0 ('b':xs) = accepts S2 xs
accepts S1 ('a':xs) = accepts S2 xs
accepts S1 ('b':xs) = accepts S0 xs
accepts S2 ('a':xs) = accepts S0 xs
accepts S2 ('b':xs) = accepts S2 xs
accepts S2 _        = True
accepts _ _         = False

xekoukou

apostolis@Geraki:~/WorkSpace$ opam install uunf uucp uutf
[NOTE] Package uutf is already installed (current version is 1.0.1).
[NOTE] Package uucp is already installed (current version is 11.0.0).
The following actions will be performed:
  ∗ install   uunf 11.0.0
  ↻ recompile uucp 11.0.0
===== ∗ 1   ↻ 1 =====
Do you want to continue? [Y/n] y

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>