<html>
<head>
<title>CRefine</title>
<link rel="stylesheet" type="text/css" href="../../style.css" />
</head>
<body>
<table>
<tr height="10">
<td>
</td>
</tr>
<tr>
<td class="tituloAzul">
Desenvolvimento
</td>
</tr>
<tr>
<td class="grande" width="500">
<br>
<div align="justify"> Após a especificação original ter sido carregada,
iniciamos a etapa de refinamento. Assim, partimos de uma especificação abstrata, geralmente centralizada,
e através de sucessivas aplicações de leis de refinamento, passamos para um estado
concreto, possivelmente distribuída.
<br>
<h5>Aplicando Lei</h5>
Para aplicarmos uma lei, devemos selecionar um termo específico. Essa seleção
é realizada sobre as linhas da janela <a href="../gui/development.html" target="body">
Desenvolvimento</a>; segure a tecla CTRL e clique na primeira e na última linha para selecionar múltiplas linhas.
<br>
<br>
<img border = "0" src="../images/selection.jpg" align="center">
<br>
<br>
Uma vez selecionado o termo, a ferramenta nos permite verificar através do Popup Menu, quais
leis são aplicáveis àquele termo. Para visualizar o PopUp Menu, clique no botão da direita sobre a seleção na
janela de Desenvolvimento. Caso exista alguma lei aplicável ao termo selecionado, as linhas que determinam esse termo
serão todas selecionadas.
<br>
Para selecionarmos e aplicarmos uma lei devemos, Devemos ir no Menu de "Aplicar Lei" e selecionar a lei desejada.
<br>
<br>
<img border = "0" src="../images/selectionlaw.jpg" align="center">
<br>
<br>
Também podemos selecionar a lei, através do Textfield presente no
Toolbar da janela principal. Para isto devemos clicar com o botão esquerdo
no mesmo.
<br>
<br>
<img border = "0" src="../images/selectionlaw2.jpg" align="center">
<br>
<br>
Ao clicarmos no mesmo, um PopUp Menu de leis, será exibido. Tal menu contém
uma classificação de leis que facilitam a sua seleção, dado a grande quantidade
de leis.
<br>
<br>
<img border = "0" src="../images/selectionlaw3.jpg" align="center">
<br>
<br>
Após a devida lei ser selecionada, o TextField guardará o nome da lei.
No caso dessa lei ser aplicável ao termo selecionado, o botão de <img border =
"0" src="../../../images/generate.gif" align="center">
será habilitado, permitindo que haja aplicação da lei selecionada.
<br>
<br>
<img border = "0" src="../images/butaoapply.jpg" align="center">
<br>
<br>
A aplicação da lei poderá ser efetuada tanto pelo clique no botão de aplicação de lei,
quanto pela opção de aplicar lei referente ao Popup Menu associado ao TextField. Para visualizarmos
tal Popup Menu, devemos clicar com o botão direito no TextField. Caso o termo selecionado
unifique o termo que a lei é aplicável, as linhas referentes a esse termo são todas
selecionadas e a opção de "Aplicar Lei" é habilitada. Tal Popup Menu também apresenta uma opção para
ver os <a href="../utils/law-details.html" target="body"> Detalhes da Lei</a>
<br>
<br>
<img border = "0" src="../images/applyLaw.jpg" align="center">
<br>
<br>
Algumas leis necessitam que certos argumentos sejam passados como
parâmetros. Para cada argumento uma pequena janela é exibida para que o
usuário passe o mesmo. Inicialmente a janela está habilitada para receber
um argumento passado no formato LaTeX.
<br>
<br>
<img border = "0" src="../images/param.jpg" align="center">
<br>
<br>
No entanto, o argumento também poderá ser digitado em Unicode,
o usuário deverá apenas setar a opção de Unicode no ComboBox da janela
Parâmetro. A inserção de símbolos Unicode é realizada através do <a href=
"../utils/virtual-keyboard.html" target="body"> Teclado Virtual</a>
<br>
Depois que os argumentos necessários são passados, a aplicação da
lei é concluída. Nesse momento, as janelas Desenvolvimento e <a href=
"../gui/code.html" target="body"> Código</a> são atualizadas. A janela
<a href="../gui/proofobligation.html" target="body"> Obrigação de Prova</a>
também pode ser atualizada caso a aplicação de lei gere alguma obrigação de
prova. Ao final da janela de <a href="../gui/development.html" target="body">
Desenvolvimento</a>, o nome da lei que foi aplicada é exibida, junto do tipo
de aplicação de lei: simulação, refinamento ou equivalência. Através da seleção
dessa da linha que contém a aplicação de lei e do Popup Menu associado a janela de
Desenvolvimento, podemos ver os <a href="../utils/law-details.html" target="body">
Detalhes da Lei.</a> Em seguida, o termo que a lei gera é exibido ao final do
refinamento.
<br>
<br>
<img border = "0" src="../images/lawapply.jpg" align="center">
<br>
<br>
<br>
<h5>Coletando Código</h5>
Eventualmente, para aplicarmos certas leis a alguns termos cujos filhos
foram alvos de aplicações de leis, devemos capturar a nova instância desses termos.
Tal atividade é realizada através de uma Coleta de Código. Tal coleta é baseada
em dois tipos de termos: Acoes e Processos.
<br>
Para realizarmos uma Coleta de Código devemos primeiramente selecionar o tipo
de coleta, ou seja, Coleta de Ação ou Coleta de Processo. Para isto, seleciona-se
o tipo desejado no primeiro ComboBox pertecente ao ToolBar da janela Principal do
CRefine.
<br>
<br>
<img border = "0" src="../images/optionsCollect.jpg" align="center">
<br>
<br>
Após ter selecionado o tipo de Coleta de Código, o segundo ComboBox será
atualizado de acordo com o tipo de coleta que foi selecionado e as novas instâncias
da categoria de termos selecionada, estarão disponíveis para serem coletadas através
da seleção de seus nomes no segundo ComboBox do ToolBar da janela Principal.
<br>
<br>
<img border = "0" src="../images/collectTerm.jpg" align="center">
<br>
<br>
Logo após a seleção do termo que será coletado ser efetuada, apenas a janela
de Desenvolvimento sofrerá alteração. Ela apresentará uma indicação que houve Coleta
de Código e logicamente, exibirá o termo coletado ao final do refinamento.
<br>
<br>
<img border = "0" src="../images/collectedTerm.jpg" align="center">
<br>
<br>
Outra forma de se realizar uma coleta de Código é através do Popup Menu associado
a janela Desenvolvimento. Pela opção "Coletar Código" do mesmo, podemos selecionar a
a categoria de termo que será coletado: Ação ou Processo. E a partir do mesmo, seleciona-se
o termo desejado.
<br>
<br>
<img border = "0" src="../images/collectTerm2.jpg" align="center">
<br>
<br>
</div>
</td>
</tr>
</table>
</body>
</html>