//Direct and Guarded implementation defined

import raw ("scripts/effects-communication/communication.lp").
import raw ("scripts/dfa/propagation.lp").
import raw ("scripts/dfa/polymorphism.lp").
import raw ("scripts/effects-communication/config.lp").

CommGuard = type variant{Invalid, Valid, Outdated}.

CommDirect = type {
    value:: int
}.

CommGuarded = type {
    value:: int,
    state:: CommGuard
}.

guard:: commDirect {
    init=function::CommDirect{
        {value = 0}
    }
    
    read= function(vault1:: CommDirect):: int{
        (vault1::CommDirect; commop(read))["value"]      
    }
    
    write= function(vault2:: CommDirect, valueNew1:: int)::CommDirect{
        (vault2::CommDirect;dfa_pseudo(vault2)) + {value = valueNew1}::    int; commop(write); dfa_uppy(vault2)
    }
}

errorRead = function:: int { -1 }

errorWrite = function:: CommGuarded{
    {
        value = -1, 
        state = Invalid()
    }
}

guard:: commGuarded{
    init=function::CommGuarded{
        {   
            value = 0, 
            state = Invalid()
        }
    }
    
    read=function(vault3:: CommGuarded):: int {
        switch variant (vault3["state"]->whatever::CommGuard;commop(read)):: int
        case (Invalid)  { errorRead() }
        case (Outdated) { errorRead() }
        case (Valid) { vault3["value"] }
    }
    
    write=function(vault4:: CommGuarded, valueNew2:: int)::CommGuarded{
        switch variant  (vault4["state"]->whatever::CommGuard;commop(write); dfa_pseudo(vault4))::int
        case (Invalid)  {
            {value = valueNew2, state = Valid()}:: CommGuarded; dfa_uppy(vault4)
        }
        
        case (Outdated) {
            {value = valueNew2, state = Valid()}:: CommGuarded; dfa_uppy(vault4)
        }
        
        case (Valid) { errorWrite():: CommGuarded; dfa_uppy(vault4) }
    }
}

main=function(cmd:: num)::int; entry {
    x1 = init():: *; dfa_polym(ret).
    x2 = write(x1, 1)::*; dfa_polym(arg).
    
    x3 = if (cmd > 0)::int {
        y = read(x2):: int; dfa_polym(arg).
        y
        
    } else {
        z = write(x2, 2)::*; dfa_polym(arg).
        a = read(z):: int; dfa_polym(arg).
        a
    }.
    
    x3
}