//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, valueNew:: int)::CommDirect{
        (vault2::CommDirect;dfa_pseudo(vault2)) + {value = valueNew}::    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::CommGuarded;commop(read)):: int
        case (Invalid)  { errorRead() }
        case (Outdated) { errorRead() }
        case (Valid) { vault3["value"] }
    }
    
    write=function(vault4:: CommGuarded, valueNew:: int)::CommGuarded{
        switch variant  (vault4)::int
        case (Invalid)  {
            {value = valueNew, state = Valid()}
        }
        
        case (Outdated) {
            {value = valueNew, state = Valid()}
        }
        
        case (Valid) { errorWrite() }
    }
}

main=function::int; entry {
    x1 = init():: Comm; dfa_polym(ret).
    x2 = write(x1, 1)::Comm; dfa_polym(arg).
    a = read(x2):: int; dfa_polym(arg).
    a
}