# Máquina X

A Máquina-X (XM) é um modelo de computação teórico introduzido por Samuel Eilenberg em 1974. O X em Máquina-X representa o tipo de dados fundamental sobre o qual a máquina opera; por exemplo, a máquina que opera em databases (objetos do tipo database) seria chamada de database-machine. O modelo da Máquina-X é estruturalmente idêntico à máquina de estados finitos, exceto que os símbolos usados para marcar as transições da máquina denotam uma relação do tipo X->X. Realizar uma transição é equivalente a aplicar a relação que a rotulaa (computar um conjunto de mudanças ao tipo de dados X), e percorrer um caminho na máquina corresponde a aplicar todas as relações associadas, uma após a outra.

## Teoria Original

A teoria original da Máquina-X proposta por Eilenberg era um modelo geral de computação completamente teórico (subsumindo a Máquina de Turing, por exemplo), o qual admitia computações determinísticas, não-determinísticas e não-terminantes. Sua obra seminal inclui muitas variantes do modelo básico da Máquina-X, cada um dos quais generalizava uma máquina de estados finitos de uma maneira ligeiramente diferente.
No modelo mais geral, uma Máquina-X é essencialmente uma "máquina para manipular objetos do tipo X". Suponha que X é algum tipo de dados, chamado tipo de dado fundamental, e que Φ é um conjunto de relações parciais φ: X → X. Uma Máquina-X é uma máquina de estados finitos com suas transições marcadas pelas relações em Φ. Em qualquer dado estado, uma ou mais transições podem ser liberadas se algum domínio da relação associada φ$_i$ aceita (um sobconjunto dos) os valores atuais de X. Em cada ciclo, todas as transições ativadas são assumidas como utilizadas. Cada caminho reconhecido pela máquina gera uma lista φ$_1$ ... φ$_n$ de relações. Chamamos a composição φ$_1$ o ... o φ$_n$ dessas relações de caminho de relações correspondente ao caminho. O comportamento da Máquina-X é definido como a união de todos os comportamentos computados por seus caminhos de relações. De modo geral, isso é não-deterministico, uma vez que aplicar qualquer relação computa um conjunto de saídas em X. No modelo formal, todas as saídas possíveis são consideradas juntas, em paralelo.
Para fins práticos, uma Máquina-X deve descrever alguma computação finita. Uma função de codificação α: Y → X converte de alguma entrada do tipo Y para o estado inicial do tipo X, e uma função de decodificação β: X → Z converte de volta do estado final X para algum tipo de saída Z. Uma vez que o estado inicial de X é populado, a Máquina-X é executada até parar, e as saídas podem então ser observadas. De modo geral, a máquina pode entrar em deadlock (travar), livelock (nunca parar), ou executar uma ou mais computações completas. Por este motivo, pesquisas mais recentes focam em Máquinas-X determinísticas, as quais possuem um comportamento que pode ser controlado e observado mais precisamente.

### Exemplo

Um compilador com um "olho-mágico" otimizador pode ser considerado como uma máquina para otimizar a estrutura de programas. Nesse Otimizador, a função de codificação α toma o código-fonte da entrada do tipo Y (a fonte do programa) e a carrega na memória de tipo X (árvore de análise sintática). Suponha que a máquina tenha diversos estados, chamados FindIncrements, FindSubExprs e Completed. A máquina começa no estado inicial FindIncrements, o qual é conectado aos outros estados pelas transições:
A relação DoIncrement mapeia a subárvore sintática correspondendo a "x := x + 1" na subárvore otimizada "++x". A relação DoSubExpr mapeia a árvore sintática contendo múltiplas ocorrencias da mesma expressão "x + y ... x + y" em uma versão otimizada com uma variável local para armazenar as repetidas computações "z := x + y; ... z ... z". Estas relações são ativadas somente se X contiver os valores de domínio (subárvores) nas quais elas operam. As relações remanescentes SkipIncrement e SkipSubExpr são nullops (relações identidade) ativadas em casos complementares.
Assim, a máquina Otimizadora vai rodar até completar, primeiro convertendo adições triviais em incrementos (durante o estado FindIncrements), a máquina vai então mover para o estado FindSubExpres e realizar uma séria de remoções de sub-expressões comuns, seguindo depois para o estado final Completed. A função de decodificação β vai então mapear do tipo de memória X (a árvore sintática otimizada) para o tipo de saída Z (código de máquina otimizado).

### Convenção

Referindo-se ao modelo original de Eilenberg, "Máquina-X" é tipicamente escrita com um "m" minúsculo, pelo sentido de "qualquer máquina para processar X". Quando referindo-se a modelos específicos mais recentes, a convenção é de se usar o "M" maiúsculo como parte do nome próprio da variante.

## Década de 1980

O interesse nas Máquinas-X foi revivido no fim dos anos 1980 por Mike Holcombe, quando este percebeu que o modelo era ideal para especificação formal de software, pois ele claramente separa fluxo de controle de processamento. Em um nível de abstração suficientemente alto, o fluxo de controle de uma computação pode ser representado como uma máquina de estados finita, então, para completar a especificação da máquina-X, basta especificar o processamento associado com cada uma das transições da máquina. A simplicidade estrutural do modelo o faz extremamente flexível; outras ilustrações iniciais da ideia incluiam as especificações de interfaces homem-computador de Holcombe, seu modelamento de processos em bioquímica celular, e o modelamento para tomadas de decisão em sistemas de comando militar de Stannett.

## Década de 1990

Máquinas-X passaram a receber atenção renovada desde meados da década de 1990, quando a "Stream X-Machine" determinística de Gilbert Laycock serviu como base para especificação de grandes sistemas de software que são completamente testáveis. Outra variante, a "Communicating Stream X-Machine" oferece um modelo útil para testes de processos biológicos e futuros sistemas de satélites swarm.

## Década de 2000

Máquinas-X foram aplicadas a analisadores semânticos por Andras Kornai, que modelam o significado de palavras por máquinas "apontadoras", que possuem um membro do conjunto base X distinto. Aplicações para outros ramos da linguística, em particular a reformulação contemporânea de Panini foram liderados por Gerar Huet e seus colegas de trabalho.

## Principais variantes

A Máquina-X raramente é encontrada em sua forma original, mas sustenta vários modelos subsequentes de computação. O mais influente modelo em teste de software foi a "Stream X-Machine". A NASA discutiu recentemente o uso de uma combinação de "Communicating Stream X-Machines" e o processo de cálculo WSCSS no design e teste de sistemas de de satélite swarm.

### Analog X Machine (AXM)

A mais antiga variante, a máquina de tempo contínuo Analog X-Machine (AXM) foi introduzida por Mike Stannet em 1990 como um potencial modelo de computação "super-Turing"; ela é consequentemente relacionada a teoria da hipercomputação.

### Stream X-Machine (SXM)

O modelo mais comumente encontrado de variante da Máquina-X é a "Stream X-Machine" feita por Gilbert Laycock em 1993, que forma a base da teoria do teste completo de software de Mike Holcombe e Florentin Ipate, que garante propriedades de correção conhecidas, uma vez que os testes tenham acabado. A "Stream X-Machine" difere do modelo original de Eilenberg no que o tipo de dado fundamental X é da forma Out* x Mem x In*, onde In* é uma sequencia de entrada, Out* é uma sequência de saída, e Mem é a memória.
A vantagem deste modelo é que ele permite que o sistema seja dirigido, um passo por vez, através de seus estados e transições, enquanto observam-se as saídas de cada passo. Estes valores são testemunhas, que garantem que funções em particular tenham sido executadas em cada passo. Como resuldado, sistemas de software complexos podem ser decompostos em uma hierarquia de Stream-X Machines, projetadas de maneira "top-down" e testadas de maneira "bottom-up". Essa abordagem de dividir-e-conquistar para projetar e testar é apoiada pela prova da integração correta de Florentin Ipate, que prova que testar as máquinas em camada independentemente é equivalente a testar o sistema composto.

### Communicating X-Machine (CXM)

A mais antiga proposta para conectar diversas Máquinas-X em paralelo é o modelo da "Communicating X-Machine" de Judith Barnard, 1995. no qual máquinas são conectadas por canais de comunicação nomeados (conhecidos como portas); este modelo existe em ambas as variantes de tempo real e discretas. Versões mais antigas deste trabalho não são completamente formais nem mostram todas as relações de entrada/saída.
Uma "Communicating X-Machine" similar utilizando canais bufferizados foi desenvolvida por Petros Kefalas. O foco deste trabalho estava na expressividade da composição dos componentes. A abilidade de redesignar canais significava que alguns dos teoremas de teste das "Stream X-Machines" não eram transferidos.

### Communicating Stream X-Machine (CSXM)

O primeiro modelo completamente formal da composição das Máquinas-X concorrentes foi proposto em 1999 por Cristina Vertan e Horia Georgescu, com base em trabalhos anteriores sobre automatos comunicantes de Philip Bird e Anthony Cowling. No modelo de Vertan, as máquinas se comunicam indiretamente, por meio de uma matriz de comunicação compartilhada (essencialmente um array de classificação), ao invés de diretamente por meio de canais compartilhados.
Bălănescu, Cowling, Georgescu, Vertan e outros estudaram as propriedades formais deste modelo CSXM em detalhe. Completas relações de entrada/saída podem ser mostradas. A matriz de comunicação estabelece um protocolo para comunicação síncrona. A vantagem disto é que, assim, o processamente de cada máquina é desacoplado da sua comunicação, permitindo o teste separado de cada comportamento. Este modelo composicional foi provado equivalente ao padrão "Stream X-Machine", alavancando assim a teoria de testes anteriormente desenvolvida por Holcombe e Ipate.

### Object X-Machine (OXM)

Kirill Bogdanov e Anthony Simons desenvolveram diversas variantes de Máquina-X para modelar o comportamento de objetos em sistemas orientados a objetos. Este modelo difere da abordagem da "Stream X-Machine", no que o tipo de dado monolítico X é distribuído e encapsulado por diversos objetos, os quais são serialmente compostos; e sistemas são acionados por invocações de métodos e returnos, em vez de entradas e saídas. Mais trabalhos nesta área envolvem a adaptação da teoria de testes formal ao contexto de hierarquia, que particiona o estado-espaço da superclasse em objetos subclasse estendidos.
O modelo "CCS-augmented X-machine" (CCSXM) foi posteriormente desenvolvido por Simons e Stannet em 2002 para suportar o completo teste de comportamento de sistemas orientados a objetos, na presença de comunicação assíncrona. É experado que este modelo tenha alguma similaridade com a recente proposta da NASA; mas nenhuma comparação definitiva entre os dois modelos foi feita até hoje.