{*
# This file is governed by the Creative Commons license
#   Attribution-NonCommercial 4.0 Unported
#   http://creativecommons.org/licenses/by-nc/4.0/
#   http://creativecommons.org/licenses/by-nc/4.0/legalcode
#
# Extended licenses, in particular commercial licenses, can be obtained from the
# author of the source code.
# Any re-distribution as source code must acknowledge the original author of this file.

#
# File: deeptelos.sml.txt
# Author: Manfred Jeusfeld, manfred.jeusfeld@acm.org
# Date: 2016-03-03 (2018-11-28)
#----------------------------------------------------------------
# Formalization of most general instances offering a simple form
# of multi-level modeling. This is the original specification of DeepTelos
# as published in the DeepTelos paper at ER-2016.
*}


Proposition with
  attribute
    ISA: Proposition;  {* shall have same semantics as Telos-ISA *}
    IN: Proposition    {* relates a power type to its meta class; not identical to Telos-IN *}
end

DeepTelosRules in Class with
  rule
    mrule1: $ forall m,x,c/Proposition (x in c) and (m IN c) ==> (x ISA m) $;
    mrule2: $ forall x,c,d/Proposition (c ISA d) and (x in c)  ==> (x in d) $;
    mrule3: $ forall c,d,m,n/Proposition (m IN c) and (n IN d) and (c ISA d)  ==> (m ISA n) $ 
{*    mrule4: $ forall c,d,e/Proposition (e ISA d) and (d ISA c)  ==> (e ISA c) $ *}
end