#include <stdio.h>

#include "config.c"

// unwind must be >LEN
// cbmc --trace --function check 4.c --unwind 16 --unwinding-assertions -DCBMC -DLEN=15

int naive(char* s)
{
        // skip spaces
        while ((*s==' ') || (*s=='\t'))
                s++;

        char *tmp=s;
        // read option (a-z)
        for (;;)
        {
                if ((*s>='a') && (*s<='z'))
                {
                        s++;
                        continue;
                }
                else
                        break;
        };
        // option must be non-empty
        if (tmp==s)
                return -1;

        // skip spaces
        while ((*s==' ') || (*s=='\t'))
                s++;

        // match '='
        if (*s!='=')
                return -1;
        s++;

        // skip spaces
        while ((*s==' ') || (*s=='\t'))
                s++;

        tmp=s;
        // read option (0-9)
        for (;;)
        {
                if ((*s>='0') && (*s<='9'))
                {
                        s++;
                        continue;
                }
                else
                        break;
        };
        // option must be non-empty
        if (tmp==s)
                return -1;

        // at this point, only spaces and whitespaces are allowed
        while (*s)
        {
                if ((*s!=' ') && (*s!='\t'))
                {
                        return -1;
                };
                s++;
        };

        // all done!
        return 1;
};

#ifdef CBMC
void check()
{
        char s[LEN+1];
        s[LEN]=0;
        __CPROVER_assert (naive(s)==fsm_main(s), "assert");
};
#endif

int main()
{
//#define S " = "
#define S "b="
        printf ("%d\n", naive(S));
        printf ("%d\n", fsm_main(S));
};