[IF-ELSE] Usar flag de não atualizar para variáveis em caso de condicional ser falsa

[mttorres]

Para referênciarmos a definição no futuro:
ex:

      r = true

     if(z){
        r = false
     } 

Caso z seja válido. Gerar normalmente,

init(r_redef1):= case z_redef1 : FALSE; TRUE : r; esac;

E toda e qualque referência será feita a redefinição, como obrigamos a NÃO MUDAR OS TIPOS DE UMA VARIÁVEL o valor
caso a condição falhe vai ser o original. E podemos referênciar tranquilamenet r_redef1. Porém, se sempre atualizarmos os valores de r (na tabela de simbolos da linguagem), se em algum futuro existir uma condição ou atribuição que referêncie essa variável pode ser que usemos os valores ERRADOS. (Pode ser que não porque BINDS de variáveis são sempre o próprio nome ativo dela). (Só o que ia ficar errado mesmo é a tabela de simbolos da linguagem, o que não é importante se a linguagem não for "uma linguagem" e só um tradutor para smv).

Na verdade, pode ser muito perigoso não tratar esse caso, pois poderia fazer funções (type-sets) terem retornos incorretos.
Porque ai a variável de retorno poderia ter valores que não foram passados de verdade (veio de um if de condição falsa ou else).

A ideia é que:

O valor da variável (mudado ou inicializado) dentro de um escopo cuja condição não é verdadeira não deve refletir na tabela de simbolos global.

• Caso seja uma redefinição ou atualização de variável (variável existe fora daquele if/else):

  • Deve escrever no nuXmv como sempre faz
  • Não deve atualizar o valor original na entrada da tabela de simbolos.
  • Somente os internos, como contexto temporal e numero de redefinições.
  • Sem problemas aparentemente, já que a variável já existe.
  • Mesmo problema de detalhado abaixo... E se a variável for typeset ou inteiro? Necessita pré processar o intervalo de possibilidades.

• Caso seja a inicialização de uma variável

  • Deve escrever no nuXmv como sempre faz
  • Porém, se a gente não inicializar o valor não vai ser possível referênciar essa variável caso essa seja usada depois (não vai existir na tabela de simbolos), ai teremos serveros problemas para

  •     -  Ideia 1: No evalIDVAR ele deve devolver um "Objeto vázio", que só tem o bind. Na hora de uma atribuição a outro objeto o valor vai ser irrelevante, apenas o tipo e o BIND. Problema é no caso de expressões, onde essa também deveria devolver objetos vazios. Outro problema é se essa variável é usada em um IF esse deve sempre ser avaliado como falso de alguma maneira. 
        - Ideia 2: Criar a variável como o de costume PORÉM para não perdermos a referência ao nome ativo, escopo, redefinições e etc. Criar uma versão com uma flag de "não válidada"(similar a undefined ou none). Para que essa referência seria então se essa não tem "valor"?  
    
    - Ideia 3: Esse é o caso que uma variável é inicializada dentro de um escopo, ela só existe ali poderiamos deixar de vestígio mesmo. (Pode gerar fluxos errados?) SIM. Caso tenha um if mais interno que faz uso dessa, a não ser que a gente use uma flag fazendo que qualquer referência a essa em condições seja automáticamente falsa. Dessa forma, por mais que a gente guarde os valores "errados", não iriamos perder o intervalo dessa variável. podendo atualizar type-sets e intervalos de inteiros. Já que essa variável vai ser usada para sintetizar expressões possíveis também (ex: var(1) + 2,  deve adicionar 3 ao intervalo de seja lá quem for atualizado, o valor não pode ser "perdido"). 
    

Note que em ambos os casos necessitamos do objeto da variável para suas redefinições.

UPDATE:

Considerando #53:

Ideia 1:

*Podemos simplesmente não avaliar sempre que a flag estiver ativa.
*Adicionar um parâmetro no escopo (tabela de simbolos) notEvaluated

• vai verificar se a variável EXISTE ao recuperar (para não referênciar variável inexistente, como já é feito)
• ao não avaliar, não salvaremos os valores (para não interferir no fluxo do programa)
• mas salvaremos uma referência, para saber que a variável foi declarada (mas não terá nenhum valor)
• ao alguem dar eval nessa variável, vai receber um "objeto vázio".
• esse objeto só terá referência ao nome (BIND) e o tipo da variável.
• qualquer referência a esse objeto vázio (ex: condicionais, sempre será falsa)
• mas e quando fizerem referência a uma soma, divisão, subtração, multiplicação? Podemos tentar recuperar o min e
  max dos envolvidos na expressão sintetizada. Mas como recuperar? Chamar pelo nome da tabela de simbolos auxiliar(evals todos vão ter que referenciar a Smv info). E então usar os min e max envolvidos na operação (ex: min1-min2, max1+max2 e etc... ) ("herda o tipo")
• mas e quanto fizerem referência a algum type set e alguma operação associada a esse?
  Typeset vão ser strings, ou retorno de função. Retornos sempre serão avliados. Podemos tentar juntar os typesets.
  Porém ao fazer isso, "matamos" concatenar strings, porque não podemos pegar
  todas as strings de ambos typesets e concatenar criando novas. Tudo bem que com as redefiniçẽos tendo acabado,
  temos CERTEZA que a ordem de a ordem de referências do typeset seguem uma ordem, podemos só pegar a última
  de cada typeset.

Ideia 2:

Não avaliar nem escrever escopos não avliados. 
Exceto em funções, onde esses vão "ser avaliados varias vezes". Mas ai teremos que ter um controle maior em funções. 

[mttorres]

Por enquanto o que foi decidido:

• Se ele nunca entra naquela condição, não avaliar nem escrever.
• Em funções, ele pode acabar entrando na condição em uma das veze que rodar (tds). Caso entre deve-se escrever da mesma maneira. (Veja a issue [Funções] Quantas vezes essa deve ser escrita no smv? #54)