Use NVM para reanudar tenazmente la operación cada vez que se aborta

8

Intentaremos escribir un programa que recuerde lo que ha estado haciendo hasta ahora y continúe hacia su objetivo si aborta una repetición. Este es un programa tenaz . Se utilizará una memoria no volátil para almacenar información a través de ejecuciones, como una serie de citas , que son bits con la cuenta de lo que sucede al abortar. Una vez conjeturé que con N cits , cualquier objetivo hasta la longitud 2 (NK) es alcanzable, para algunos pequeños K. fijos Ahora me inclino a pensar que el objetivo no se puede lograr :-(

Se le pide un programa tenaz con objetivo 01 , que ya es un objetivo no trivial ; o una prueba rigurosa de imposibilidad.

Un programa tenaz se define como uno que:

  1. Siempre que se ejecuta , se ejecuta a partir del mismo punto de entrada, sin entrada, y puede compartir información entre ejecuciones exclusivamente por medio de N cits (definidos a continuación); cualquier otra información tiene el mismo contenido al comienzo de cada ejecución, tiene contenido impredecible al inicio de la ejecución, no se puede cambiar (el programa en sí) o no se puede leer ( salida y valor anteriores ).
  2. Es tal que cuando se ejecuta dentro de una sesión se detiene (usando una característica de su lenguaje), dentro de un retraso limitado desde el inicio de la ejecución, a menos que se cancele antes de detenerse; abort ocurre en cualquier instante arbitrario y evita la operación hasta otra ejecución (si la hay).
  3. Es tal que la concatenación en orden cronológico de los caracteres que genera es la misma cadena finita (el objetivo ) en cualquier sesión de arbitrariamente muchas ejecuciones que comprenden al menos una ejecución donde el programa se dejó en ejecución hasta que se detenga.
  4. Emite caracteres usando un dispositivo que atómicamente : recibe un valor entre 0 1 2 3 puesto por el programa y emite0(resp.1) Para valores entre 0 o 2 (resp 1 o 3) si y solo si ese valor es diferente del anterior valor puesto, se supone que es 0 para el primer puesto en una sesión.

¡Existen programas tenaces! Cualquier programa que simplemente pone un número fijo de veces un valor fijo válido, luego se detiene, es tenaz con la meta vacía (si el número o el valor es 0), 0(si el número es positivo y el valor es 2) o 1(de lo contrario). Cualquier objetivo más largo requiere NVM.

Cada cit modela un bit NVM con la cuenta del efecto de una ejecución anulada durante una escritura en el cit. En cualquier instante un cit está en uno de los tres estados posibles 0 1o U. El valor leído de un cit siempre es 0 o 1; también coincide con el estado a menos que U. Un cit se inicializa al estado 0antes de la primera ejecución en una sesión y, de lo contrario, cambia de estado solo cuando el programa ordena una escritura , con efecto dependiendo de lo que está escrito, si la ejecución se cancela durante la escritura o no, y desde estado anterior de cit:

         Former state  0   1   U    Rationale given by hardware guru
Operation
  Write 0 completed    0   0   0    Discharging returns cit to 0
  Write 0 aborted      0   U   U    Aborted discharging leaves cit unspecified
  Write 1 aborted      U   1   U    Aborted    charging leaves cit unspecified
  Write 1 completed    1   1   U    Charging a non-discharged cit is inhibited

La HAL para lo anterior se declara en C como:

/* file "hal.h"              unspecified parameter values give undefined behavior */
#define  N 26                       /* number of  cits                            */
void     p(unsigned v);             /* put value v; v<4                           */
unsigned r(unsigned i);             /* read from  cit at i; returns 0 or 1;  i<N. */
void     w(unsigned i, unsigned b); /* write b to cit at i;    b is 0 or 1;  i<N. */
/*                            all functions return in bounded time unless aborted */

Nuestro primer intento de un programa tenaz con objetivo 01es:

#include "hal.h"                    /* discount this line's length                */
main(){                             /* entry point, no parameters or input        */
    if (r(3)==0)                    /* cit 3 read as 0, that is state 0 or U      */
        w(3,0),                     /* write 0 to cit 3, to ensure state 0        */
        p(2);                       /* put 2 with output '0' initially            */
    w(3,1),                         /* mark we have output '0' (trouble spot!)    */
    p(1);                           /* put 1 with output '1'                      */
}                                   /* halt (but we can be re-run)                */

Murphy realiza una primera sesión, deja la primera carrera deteniéndose y finaliza la sesión; la salida de la sesión es la salida de una sola ejecución 01; Hasta aquí todo bien.
En otra sesión, Murphy aborta una primera carrera w(3,1), dejando a cit en estado U; en una segunda ejecución, Murphy decide que r(3)es 1 (que cit está en estado U), y deja el programa paralizado (observe cómo w(3,1)no cambió el estado de cit); en una tercera carrera, Murphy decide que r(3)es 0, aborta después p(2)y termina la sesión.
La salida concatenada de la segunda sesión es 010(un carácter por ejecución) pero es diferente de 01la primera sesión, por lo tanto, el programa no es tenaz, ya que la condición 3 no se cumple.


El lenguaje es gratuito, adapte la interfaz C según el lenguaje. Seleccionaré la mejor respuesta según el menor número de citas utilizadas; luego el menor número de escrituras en el peor de los casos desde la ejecución hasta la salida (o se detiene si no hay salida); luego el menor número de escrituras antes de detenerse en una sesión sin abortar; entonces el programa más corto. Cuente solo el código de llamada, no la interfaz o su implementación, que no es necesaria. Una prueba rigurosa de imposibilidad eliminaría cualquier programa (y sería una sorpresa para mí) ; Seleccionaría el más simple de entender.

Verifique tres veces que el programa realmente cumpla con la meta según 3, independientemente de la cantidad y los instantes de abortos; ¡eso es difícil!

Actualización: agregué una respuesta candidata . Siéntase libre de derrotarlo. ¡Oh, Hammar hizo eso en minutos usando un programa sistemático!

Estado : hasta ahora no tenemos solución; sepa con certeza que no hay solución con 1 o 2 cits; pero no tiene prueba de imposibilidad con 3 o más cits. La declaración no se ha encontrado ambigua. El problema tendría una solución si cambiamos la matriz cit ligeramente (por ejemplo, poner 1 en la parte inferior derecha, en cuyo caso el ejemplo anterior es correcto).

fgrieu
fuente
Siento que se hizo una pregunta similar, creo que tal vez se relaciona más con la memoria flash / sobretensiones, pero parece que no puedo encontrarla.
Gaffi
1
@Gaffi: Hace dos semanas hice una pregunta pidiendo un programa con propiedades similares para decimales de Pi-3 en binario a la longitud máxima posible dada una cantidad de cits y otras cosas, redactadas con corte de energía en lugar de abortar . Fue recibido con críticas (positivas) preguntando cómo se determinarían respuestas válidas. Me di cuenta de que probablemente no podría, y eliminé la pregunta. Con este código de golf meticulosamente redactado, estoy seguro de que puedo consultar el programa o publicar uno más breve y tenaz para muchos idiomas. Lo único que lamento es que debería haber hecho el gol un poco más sexy.
fgrieu
1
¿Estás seguro de que quieres que esto sea código golf? Me parece que el desafío es escribir un programa de este tipo (y demostrar su corrección); Una vez que se logra, el golf se convierte en un ejercicio bastante trivial (y algo mal definido, dado que se nos permite adaptar la interfaz). ¿Tal vez simplemente hacer que sea un desafío de código ?
Ilmari Karonen
Otra pregunta: ¿probar la imposibilidad de programas tenaces no triviales sería una solución? (Todavía no tengo tal prueba, pero estoy empezando a pensar que ese puede ser el caso.)
Ilmari Karonen
@IlmariKaronen: ¡La prueba de imposibilidad sería el rey! He publicado una solución que puede ser válida. Ver por ti mismo.
fgrieu

Respuestas:

6

Si bien no tengo una solución ni una prueba de imposibilidad, pensé que publicaría mi arnés de prueba para cualquiera que quiera jugar con esto, ya que casi me he rendido en este momento.

Es una implementación de los programas de modelado HAL como una mónada Haskell. Comprueba la tenacidad haciendo una búsqueda amplia de las posibles sesiones para comprobar si las sesiones 1. se han detenido una vez sin producir la salida correcta, o 2. han producido una salida que no es un prefijo de la deseada (esto también atrapa programas que producen una salida infinita).

{-# LANGUAGE GADTs #-}

module HAL where

import Control.Monad
import Data.List

import Data.Map (Map)
import qualified Data.Map as Map

import Data.Set (Set)
import qualified Data.Set as Set

newtype CitIndex = Cit Int
  deriving (Eq, Ord, Show)

data CitState = Stable Int | Unstable
  deriving (Eq, Ord, Show)

data Program a where
  Return :: a -> Program a
  Bind :: Program a -> (a -> Program b) -> Program b
  Put :: Int -> Program ()
  Read :: CitIndex -> Program Int
  Write :: CitIndex -> Int -> Program ()
  Log :: String -> Program ()
  Halt :: Program ()

instance Monad Program where
  return = Return
  (>>=) = Bind

data Session = Session
  { cits :: Cits
  , output :: [Int]
  , lastPut :: Int
  , halted :: Bool
  } deriving (Eq, Ord, Show)

data Event
  = ReadE CitIndex Int
  | PutE Int
  | WriteSuccessE CitIndex Int
  | WriteAbortedE CitIndex Int
  | LogE String
  | HaltedE
  deriving (Eq, Ord, Show)

type Log = [(Event, Cits)]

check :: Program () -> Int -> [Int] -> IO ()
check program n goal =
  case tenacity (program >> Halt) goal of
    Tenacious  -> putStrLn "The program is tenacious."
    Invalid ss -> do
      putStrLn "The program is invalid. Example sequence:"
      forM_ (zip [1..] ss) $ \(i, (log, s)) -> do
        ruler
        putStrLn $ "Run #" ++ show i ++ ", Initial state: " ++ formatState n s
        ruler
        mapM_ (putStrLn . formatEvent n) log
  where ruler = putStrLn $ replicate 78 '='

run :: Program a -> Session -> [(Maybe a, Log, Session)]
run (Return x) s = [(Just x, [], s)]
run (Bind x f) s = do
  (r1, l1, s1) <- run x s
  case r1 of
    Just y  -> [(r2, l1 ++ l2, s2) | (r2, l2, s2) <- run (f y) s1]
    Nothing -> [(Nothing, l1, s1)]
run (Put x) s = [(Just (), [(PutE x, cits s)], s')]
  where s' | lastPut s /= x = s { lastPut = x, output = output s ++ [x `mod` 2] }
           | otherwise      = s
run (Read cit) s =
  case lookupCit cit (cits s) of
    Stable x -> [(Just x, [(ReadE cit x, cits s)], s)]
    Unstable -> [(Just x, [(ReadE cit x, cits s)], s) | x <- [0, 1]]
run (Write cit x) (s @ Session { cits = cits }) =
  [(Just (), [(WriteSuccessE cit x, completed)], s { cits = completed }),
   (Nothing, [(WriteAbortedE cit x, aborted  )], s { cits = aborted })]
  where state = lookupCit cit cits
        completed = updateCit cit newState cits 
          where newState = case (x, state) of
                             (0, _)        -> Stable 0
                             (1, Unstable) -> Unstable
                             (1, Stable _) -> Stable 1

        aborted = updateCit cit newState cits
          where newState = case (x, state) of
                             (0, Stable 0) -> Stable 0
                             (0, _)        -> Unstable
                             (1, Stable 1) -> Stable 1
                             (1, _)        -> Unstable
run (Halt) s = [(Just (), [(HaltedE, cits s)], s { halted = True })] 
run (Log msg) s = [(Just (), [(LogE msg, cits s)], s)]

newSession :: Session
newSession = Session
  { cits = initialCits
  , output = []
  , lastPut = 0
  , halted = False }

newtype Cits = Cits (Map CitIndex CitState)
  deriving (Eq, Ord, Show)

initialCits = Cits (Map.empty)

lookupCit :: CitIndex -> Cits -> CitState
lookupCit cit (Cits m) = Map.findWithDefault (Stable 0) cit m

updateCit :: CitIndex -> CitState -> Cits -> Cits
updateCit index (Stable 0) (Cits m) = Cits $ Map.delete index m 
updateCit index newState (Cits m) = Cits $ Map.insert index newState m

data Tenacity = Tenacious | Invalid [(Log, Session)]
  deriving (Eq, Ord, Show)

tenacity :: Program () -> [Int] -> Tenacity
tenacity program goal = bfs Set.empty [(newSession, [])]
  where
    bfs :: Set Session -> [(Session, [(Log, Session)])] -> Tenacity
    bfs visited [] = Tenacious
    bfs visited ((s, pred) : ss)
      | Set.member s visited = bfs visited ss
      | valid s   = bfs (Set.insert s visited) $ ss ++ [(s', (l, s) : pred) | (_, l, s') <- run program s]
      | otherwise = Invalid $ reverse (([], s) : pred)

    valid :: Session -> Bool
    valid Session { output = output, halted = halted }
      | halted    = output == goal
      | otherwise = output `isPrefixOf` goal

formatState :: Int -> Session -> String
formatState n s = "[cits: " ++ dumpCits n (cits s) ++ "] [output: " ++ dumpOutput s ++ "]"

formatEvent :: Int -> (Event, Cits) -> String
formatEvent n (event, cits) = pad (78 - n) text ++ dumpCits n cits 
  where text = case event of
                 ReadE (Cit i) x         -> "read " ++ show x ++ " from cit #" ++ show i
                 PutE x                  -> "put " ++ show x
                 WriteSuccessE (Cit i) x -> "wrote " ++ show x ++ " to cit #" ++ show i
                 WriteAbortedE (Cit i) x -> "aborted while writing " ++ show x ++ " to cit #" ++ show i
                 LogE msg                -> msg
                 HaltedE                 -> "halted"

dumpCits :: Int -> Cits -> String
dumpCits n cits = concat [format $ lookupCit (Cit i) cits | i <- [0..n-1]]
  where format (Stable i) = show i
        format (Unstable) = "U" 

dumpOutput :: Session -> String
dumpOutput s = concatMap show (output s) ++ " (" ++ show (lastPut s) ++ ")"

pad :: Int -> String -> String
pad n s = take n $ s ++ repeat ' '

Aquí está el programa de ejemplo dado por el OP convertido a Haskell.

import Control.Monad (when)

import HAL

-- 3 cits, goal is 01
main = check example 3 [0, 1]

example = do
  c <- Read (Cit 2)
  d <- Read (Cit c)
  when (0 == c) $ do
    Log "in first branch"
    Write (Cit 2) 0
    Write (Cit 1) 0
    Write (Cit 1) (1 - d)
    Write (Cit 2) 1
  Write (Cit 0) 0
  when (d == c) $ do
    Log "in second branch"
    Put 2
    Write (Cit 2) 0
  Write (Cit 0) 1
  Put 1

Y aquí está el resultado correspondiente, que muestra que el programa no es tenaz.

The program is invalid. Example sequence:
==============================================================================
Run #1, Initial state: [cits: 000] [output:  (0)]
==============================================================================
read 0 from cit #2                                                         000
read 0 from cit #0                                                         000
in first branch                                                            000
wrote 0 to cit #2                                                          000
wrote 0 to cit #1                                                          000
wrote 1 to cit #1                                                          010
wrote 1 to cit #2                                                          011
wrote 0 to cit #0                                                          011
in second branch                                                           011
put 2                                                                      011
wrote 0 to cit #2                                                          010
wrote 1 to cit #0                                                          110
put 1                                                                      110
halted                                                                     110
==============================================================================
Run #2, Initial state: [cits: 110] [output: 01 (1)]
==============================================================================
read 0 from cit #2                                                         110
read 1 from cit #0                                                         110
in first branch                                                            110
wrote 0 to cit #2                                                          110
wrote 0 to cit #1                                                          100
wrote 0 to cit #1                                                          100
aborted while writing 1 to cit #2                                          10U
==============================================================================
Run #3, Initial state: [cits: 10U] [output: 01 (1)]
==============================================================================
read 1 from cit #2                                                         10U
read 0 from cit #1                                                         10U
wrote 0 to cit #0                                                          00U
aborted while writing 1 to cit #0                                          U0U
==============================================================================
Run #4, Initial state: [cits: U0U] [output: 01 (1)]
==============================================================================
read 0 from cit #2                                                         U0U
read 0 from cit #0                                                         U0U
in first branch                                                            U0U
wrote 0 to cit #2                                                          U00
wrote 0 to cit #1                                                          U00
wrote 1 to cit #1                                                          U10
wrote 1 to cit #2                                                          U11
wrote 0 to cit #0                                                          011
in second branch                                                           011
put 2                                                                      011
wrote 0 to cit #2                                                          010
wrote 1 to cit #0                                                          110
put 1                                                                      110
halted                                                                     110
==============================================================================
Run #5, Initial state: [cits: 110] [output: 0101 (1)]
==============================================================================
hammar
fuente
4

A menos que alguien pueda encontrar un error en este programa, creo que verifica y rechaza todos los programas relevantes de dos cit.

Sostengo que es suficiente considerar los programas que leen todos los cits y activan un número formado por el conjunto. Cada rama del interruptor será una serie de escrituras y puts. Nunca tiene sentido poner el mismo número más de una vez en una rama, o poner el segundo dígito de salida antes del primero. (Estoy moralmente seguro de que no hay ningún punto que muestre el primer dígito que no sea al comienzo de una rama o el segundo dígito que no sea al final, pero por ahora estoy evitando esa simplificación).

Luego, cada rama tiene un conjunto objetivo de cits que quiere establecer, y se mueve hacia él estableciendo los bits que quiere que sean 0 como 0, y los bits que quiere que sean 1 como 0 y luego 1; Estas operaciones de escritura se pueden ordenar de varias maneras. No tiene sentido establecer un bit en 1 a menos que ya lo haya establecido en 0 en esa ejecución, o es probable que sea un nop.

Considera 13680577296 posibles programas; Le tomó a una máquina de 4 núcleos un poco menos de 7 horas verificarlos a todos sin encontrar una sola solución.

import java.util.*;

// State is encoded with two bits per cit and two bits for the output state.
//    ... [c_2=U][c_2=1/U][c_1=U][c_1=1/U][output_hi][output_lo]
// Output state must progress 0->1->2.
// Instruction (= program branch) is encoded with three or four bits per step.
//      The bottom two bits are the cit, or 0 for output/loop
//      If they're 0, the next two bits are 01 or 10 for output state, or 11 for halt.
//      Otherwise the next two bits are the value to write to the cit.
public class CitBruteForcer implements Runnable {

    static final int[] TRANSITION_OK = new int[]{
        // Index: write curr_hi curr_lo
        0,  // write 0 to 0 => 0
        0,  // write 0 to 1 => 0
        0,  // write 0 to U => 0
        -1, // invalid input
        1,  // write 1 to 0 => 1
        1,  // write 1 to 1 => 1
        2,  // write 1 to U => U
        -1  // invalid input
    };
    static final int[] TRANSITION_ABORT = new int[]{
        // Index: write curr_hi curr_lo
        0,  // write 0 to 0 => 0
        2,  // write 0 to 1 => U
        2,  // write 0 to U => U
        -1, // invalid input
        2,  // write 1 to 0 => U
        1,  // write 1 to 1 => 1
        2,  // write 1 to U => U
        -1  // invalid input
    };

    private final int[] possibleInstructions;
    private final int numCits, offset, step;
    private long tested = 0;

    private CitBruteForcer(int numCits, int[] possibleInstructions, int offset, int step)
    {
        this.numCits = numCits;
        this.possibleInstructions = possibleInstructions;
        this.offset = offset;
        this.step = step;
    }

    public void run()
    {
        int numStates = 1 << numCits;
        int n = possibleInstructions.length;
        long limit = pow(n, numStates);

        for (long i = offset; i < limit; i += step) {
            // Decode as a base-n number.
            int[] instructions = new int[numStates];
            long tmp = i;
            for (int j = 0; j < numStates; j++, tmp /= n) instructions[j] = possibleInstructions[(int)(tmp % n)];
            Program p = new Program(numCits, instructions);
            if (p.test()) System.out.println("Candidate: " + i);
            tested++;
        }
    }

    public static void main(String[] args) {
        int numCits = 2;
        int numThreads = 4;
        int[] possibleInstructions = buildInstructions(numCits);

        int numStates = 1 << numCits;
        int n = possibleInstructions.length;
        System.out.println(n + " possible instructions");
        long limit = pow(n, numStates);

        CitBruteForcer[] forcers = new CitBruteForcer[numThreads];
        for (int i = 0; i < numThreads; i++) {
            forcers[i] = new CitBruteForcer(numCits, possibleInstructions, i, numThreads);
            new Thread(forcers[i]).start();
        }

        int pc = 0;
        while (pc < 100) {
            // Every 10 secs is easily fast enough to update
            try { Thread.sleep(10000); } catch (InterruptedException ie) {}

            long tested = 0;
            for (CitBruteForcer cbf : forcers) tested += cbf.tested; // May underestimate because the value may be stale
            int completed = (int)(100 * tested / limit);
            if (completed > pc) {
                pc = completed;
                System.out.println(pc + "% complete");
            }
        }
        System.out.println(limit + " programs tested");
    }

    private static int[] buildInstructions(int numCits) {
        int limit = (int)pow(3, numCits);
        Set<Integer> instructions = new HashSet<Integer>();
        for (int target = 0; target <= limit; target++) {
            int toSetZero = 0, toSetOne = 0;
            for (int i = 0, tmp = target; i < numCits; i++, tmp /= 3) {
                if (tmp % 3 == 0) toSetZero |= 1 << i;
                else if (tmp % 3 == 1) toSetOne |= 1 << i;
            }
            buildInstructions(0xc, toSetZero, toSetOne, false, false, instructions);
        }
        int[] rv = new int[instructions.size()];
        Iterator<Integer> it = instructions.iterator();
        for (int i = 0; i < rv.length; i++) rv[i] = it.next().intValue();
        return rv;
    }

    private static void buildInstructions(int suffix, int toSetZero, int toSetOne, boolean emitted0, boolean emitted1, Set<Integer> instructions)
    {
        if (!emitted1) {
            buildInstructions((suffix << 4) + 0x8, toSetZero, toSetOne, false, true, instructions);
        }
        if (!emitted0) {
            buildInstructions((suffix << 4) + 0x4, toSetZero, toSetOne, true, true, instructions);
        }
        if (toSetZero == 0 && toSetOne == 0) {
            instructions.add(suffix);
            return;
        }

        for (int i = 0; toSetZero >> i > 0; i++) {
            if (((toSetZero >> i) & 1) == 1) buildInstructions((suffix << 3) + 0x0 + i+1, toSetZero & ~(1 << i), toSetOne, emitted0, emitted1, instructions);
        }
        for (int i = 0; toSetOne >> i > 0; i++) {
            if (((toSetOne >> i) & 1) == 1) buildInstructions((suffix << 3) + 0x4 + i+1, toSetZero | (1 << i), toSetOne & ~(1 << i), emitted0, emitted1, instructions);
        }
    }

    private static long pow(long n, int k) {
        long rv = 1;
        while (k-- > 0) rv *= n;
        return rv;
    }

    static class Program {
        private final int numCits;
        private final int[] instructions;
        private final Set<Integer> checked = new HashSet<Integer>();
        private final Set<Integer> toCheck = new HashSet<Integer>();

        Program(int numCits, int[] instructions) {
            this.numCits = numCits;
            this.instructions = (int[])instructions.clone();
            toCheck.add(Integer.valueOf(0));
        }

        boolean test() {
            try {
                while (!toCheck.isEmpty()) checkNext();
            } catch (Exception ex) {
                return false;
            }

            // Need each reachable state which hasn't emitted the full output to be able to reach one which has.
            Set<Integer> reachable = new HashSet<Integer>(checked);
            for (Integer reached : reachable) {
                checked.clear();
                toCheck.clear();
                toCheck.add(reached);
                while (!toCheck.isEmpty()) checkNext();
                boolean emitted = false;
                for (Integer i : checked) {
                    if ((i.intValue() & 3) == 2) emitted = true;
                }
                if (!emitted) return false;
            }

            return true;
        }

        private void checkNext() {
            Integer state = toCheck.iterator().next();
            toCheck.remove(state);
            checked.add(state);
            run(state.intValue());
        }

        private void run(final int state) {
            // Check which instructions apply
            for (int i = 0; i < instructions.length; i++) {
                boolean ok = true;
                for (int j = 1; j <= numCits; j++) {
                    int cit = (state >> (2 * j)) & 3;
                    if (cit == 2 || cit == ((i >> (j-1)) & 1)) continue;
                    ok = false; break;
                }
                if (ok) run(state, instructions[i]);
            }
        }

        private void run(int state, int instruction) {
            while (true) {
                int cit = instruction & 3;
                if (cit == 0) {
                    int emit = (instruction >> 2) & 3;
                    if (emit == 3) break;
                    if (emit > (state & 3) + 1 || emit < (state & 3)) throw new IllegalStateException();
                    state = (state & ~3) | emit;
                    instruction >>= 4;
                }
                else {
                    int shift = 2 * cit;
                    int transitionIdx = (instruction & 4) + ((state >> shift) & 3);
                    int stateMasked = state & ~(3 << shift);
                    consider(stateMasked | (TRANSITION_ABORT[transitionIdx] << shift));
                    state = stateMasked | (TRANSITION_OK[transitionIdx] << shift);
                    instruction >>= 3;
                }
                // Could abort between instructions (although I'm not sure this is strictly necessary - this is "better" than the mid-instruction abort
                consider(state);
            }
            // Halt or loop.
            consider(state);
        }

        private void consider(int state) {
            if (!checked.contains(state)) toCheck.add(state);
        }
    }
}
Peter Taylor
fuente
Si uso mi suposición sobre la ubicación de las salidas, la cantidad de programas de 2-cit disminuye considerablemente y el tiempo de verificación es inferior a un minuto, pero incluso con esta suposición, la cantidad de programas de 3-cit es superior a 2 ^ 80, o un factor de aproximadamente 2 ^ 47 más que los programas de 2-cit verificados en 7 horas. No razonablemente fuerza bruta, en otras palabras.
Peter Taylor
0

Este es mi mejor intento de responder a mi propia pregunta. No estoy seguro de que cumpla con el requisito 3, y estoy abierto a la refutación. No es tenaz :-(

/*  1 */    #include "hal.h"
/*  2 */    main(){
/*  3 */        unsigned c = r(2);  // get cit 2 into c
/*  4 */        unsigned d = r(c);  // get cit c into d
/*  5 */    // here if d==c then we have not output 1 yet  
/*  6 */    //              else we have     output 0   
/*  7 */        if (0==c)
/*  8 */            w( 2, 0 ),      // cit 2 to 0
/*  9 */            w( 1, 0 ),      // cit 1 to 0
/* 10 */            w( 1,!d ),      // cit 1 to complement of d
/* 11 */            w( 2, 1 );      // cit 2 to 1
/* 12 */        w( 0, 0 );          // cit 0 to 0
/* 13 */        if (d==c)
/* 14 */            p( 2 ),         // put 2, first one outputs 0
/* 15 */            w( 2, 0 );      // cit 2 to 0
/* 16 */        w( 0, 1 );          // cit 0 to 1
/* 17 */        p( 1 );             // put 1, first one outputs 1
/* 16 */    }                       // halt
fgrieu
fuente
2
Mi programa de prueba dice que no es tenaz: 1. Ejecute el programa hasta su finalización. Salida: 01,: Cits 110. 2. Abortar durante el # 15. Cits: 10U. 3. Leer c = 1, abortar durante el n. ° 12. Cits: U0U. 4. Lea c = 0, d = 0y el programa se imprimirá 01nuevamente.
hammar
Lo sentimos, el primer aborto debe estar en la línea # 11, no en la # 15.
hammar