system implementation sys.impl
    parameters
        C0: set of indices;
        trustedClients0: set indexed by C0 of bool;
        connectedTo0: set indexed by C0 of index;
        S: set of indices;
        trustedServers: set indexed by S of bool;
        protected: bool;

    initial
        not protected
        and forall(c in C0, forall (s in S, (not trustedClients0[c] and s = connectedTo0[c]) -> (not trustedServers[s])))
        and forall(c in C0, forall (s not in S, s != connectedTo0[c]));

    subcomponents
        d: system databaseServer;
        servers: set indexed by S of system applicationServer;
        clients0: set indexed by C0 of system Client;
        e: system Evil;

    connections
        d -> servers[s] if protected and trustedServers[s] for s in S;
        servers[s] -> clients0[c] if s = connectedTo0[c] for s in S, c in C0;
        clients0[c] -> clients0[d] if not trustedClients0[c] for c in C0, d in C0;
        clients0[c] -> e if not trustedClients0[c] for c in C0;

    reconfigurations
        next(protected) = true;
        exists(s not in S, next(S) = add(S, s) and next(trustedServers[s]) = true);
        exists(s in S, not protected and next(trustedServers[s]) = false);

        exists(s in S, exists (c not in C0, not trustedServers[s] and next(C0) = add(C0, c) and next(connectedTo0[c]) = s and next(trustedClients0[c]) = false));

        exists(s in S, exists (c not in C0, trustedServers[s] and next(C0) = add(C0, c) and next(connectedTo0[c]) = s and next(trustedClients0[c]) = true));

        exists(s in S, exists (c in C0, trustedClients0[c] and next(connectedTo0[c]) = s));

        exists(s in S, exists (c in C0, not trustedClients0[c] and not trustedServers[s] and next(connectedTo0[c]) = s));

        exists(s in S, exists (c in C0, not trustedClients0[c] and not protected and next(connectedTo0[c]) = s and next(trustedServers[s]) = false));

        exists(s in S, exists (c in C0, trustedClients0[c] and s = connectedTo0[c] and not protected and next(trustedClients0[c]) = false and next(trustedServers[s]) = false));
end sys.impl;
