Horrible Python code that generates horrible NuSMV code to check a horrible elevator specification

bad.py

class Mstr:
    def __init__(self, initial=''):
        if isinstance(initial, Mstr):
            self.content = initial.content
        elif isinstance(initial, str):
            self.content = [initial]
        elif hasattr(initial, '__iter__'):
            self.content = [str(x) for x in initial]
        else:
            self.content = [str(initial)]

    def __add__(self, other):
        if isinstance(other, Mstr):
            return Mstr([x + y for x in self.content for y in other.content])
        else:
            return Mstr(self + Mstr(other))

    def __getitem__(self, i):
        return self.content[i]

    def __iter__(self):
        return iter(self.content)

    def __str__(self):
        return ''.join(self.content)

def mstr(*args):
    r = Mstr()
    for arg in args:
        r += arg
    return str(r)

n = 10
n_users = 3

varlist = ['doorOpen', 'lightOutside', 'lightInside', 'buttonOutside',
'buttonInside', 'atFloor']
varpass = ', '.join(varlist)

def joinfs(*args):
    global n
    return '\n  SPEC (' + ') & ('.join([str(i).join(args)
        for i in range(n)]) + ')'

thing = mstr(
'''MODULE main -- elevator
  VAR
    atFloor : 0..''', n-1, ';') + \
mstr('\n    ', varlist[:5], ' : array 0..', n-1, ' of boolean;')
for i in range(n_users):
    thing += mstr('\n    user', i, ' : process user(', varpass, ');')

thing += mstr('\n    controller : process controller(', varpass, ');') + \
mstr('''
  ASSIGN
    init(atFloor) := ''', str(set(range(n))), ';') + mstr('\n    init(',
            varlist[0:5], '[', range(n), ']) := FALSE;')
thing += joinfs('AG(!(atFloor = ', ') -> !doorOpen[', '])')
thing += joinfs('AG(buttonInside[', '] -> A[lightInside[', '] U (atFloor = ',
            ' & doorOpen[', '])])')
thing += joinfs('AG((atFloor = ', ' & doorOpen[', ']) -> !lightInside[',
            '])')
thing += joinfs('AG((atFloor = ', ' & doorOpen[', ']) -> A[!lightInside[',
    '] U buttonInside[', ']])')
thing += joinfs('AG((buttonInside[', '] & (atFloor = ', ' & doorOpen[',
    '])) -> lightInside[', '])')
thing += joinfs('AG(buttonOutside[', '] -> A[lightOutside[', '] U (atFloor = ',
            ' & doorOpen[', '])])')
thing += joinfs('AG((atFloor = ', ' & doorOpen[', ']) -> !lightOutside[',
            '])')
thing += joinfs('AG((atFloor = ', ' & doorOpen[', ']) -> A[!lightOutside[',
    '] U buttonOutside[', ']])')
thing += joinfs('AG((buttonOutside[', '] & (atFloor = ', ' & doorOpen[',
    '])) -> lightOutside[', '])')
thing += joinfs('AG((!lightInside[', '] & !lightOutside[', '] & !(atFloor = ',
    ' & doorOpen[', '])) -> A[!(atFloor = ', ' & doorOpen[',
    ']) U (buttonInside[', '] | buttonOutside[', '])])')
thing += joinfs('AG((' + ' & '.join(Mstr('!lightInside[') + range(n) + ']') +
    ' & ' + ' & '.join(Mstr('!lightOutside[') + range(n) + ']') +
    ' & atFloor = ', ') -> A[atFloor = ', ' U (' +
    ' | '.join(Mstr('lightInside[') + range(n) + ']') + ' | ' +
    ' | '.join(Mstr('lightOutside[') + range(n) + ']') + ')])')
thing += joinfs('AG(lightInside[', '] -> AF(atFloor = ', ' & doorOpen[',
        ']))')
thing += joinfs('AG(lightOutside[', '] -> AF(atFloor = ', ' & doorOpen[',
        ']))')
thing += mstr('''
MODULE controller(''', varpass, ''')
  VAR
    goingUp : boolean;
  ASSIGN
    init(goingUp) := TRUE;''') + \
mstr([mstr('\n    next(light', side, '[', i, ']) := (light', side, '[', i,
    '] | button', side, '[', i,
    ']) & !(atFloor = ', i, ');')
    for side in ['Outside', 'Inside'] for i in range(n)]) + \
mstr([mstr('\n    next(doorOpen[', i, ']) := atFloor = ', i, ' & (lightInside[',
    i, '] | lightOutside[', i, ']);') for i in range(n)]) + \
mstr('''
    next(atFloor) :=
      case''')
for going, target, step in [('goingUp', n, 1), ('!goingUp', -1, -1)]:
    thing += mstr('''
        ''', going, ''' :
          case''')
    for i in range(n):
        thing += mstr('''
            atFloor = ''', i, ''' :
              case''')
        for j in range(i, target, step):
            thing += mstr('''
                lightInside[''', j, '] | lightOutside[', j,
                '] : ', j, ';')
        thing += mstr('''
                TRUE : ''', i, ''';
              esac;''')
    thing += mstr('''
          esac;''')
thing += mstr('''
      esac;
    next(goingUp) :=
      case''')
for going, target, step, alt, default in \
        [('goingUp', n, 1, n-1, 'FALSE'), ('!goingUp', -1, -1, 0, 'TRUE')]:
    thing += mstr('''
        ''', going, ''' :
          case
            atFloor = ''', alt, ' : ', default, ';')
    for i in range(n):
        if i == alt: continue
        thing += mstr('''
            atFloor = ''', i, ' : ',
            ' | '.join([mstr('lightInside[', j, '] | lightOutside[', j, ']')
                for j in range(i+step, target, step)]), ';')
    thing += mstr('''
          esac;''')
thing += mstr('''
      esac;
MODULE user(''', varpass, ''')
  VAR
    inside : boolean;
    floor : 0..''', n-1, ''';
    dest : 0..''', n-1, ''';
  ASSIGN
    init(floor) := ''', str(set(range(n))), ''';
    init(dest) := ''', str(set(range(n))), ''';
    init(inside) := FALSE;''')
for bside, iside, x in [('Outside', '!inside', 'floor'),
        ('Inside', 'inside', 'dest')]:
    for floor in range(n):
        thing += mstr('''
    next(button''', bside, '[', floor, ']) := ', iside, ' & !light', bside,
        '[', floor, '] & !(atFloor = ', floor, ' & doorOpen[', floor,
        ']) & ', x, ' = ', floor, ';')
thing += mstr('''
    next(floor) :=
      case
        inside : atFloor;
        !inside : floor;
      esac;
    next(dest) :=
      case
        floor = dest & !inside : ''', str(set(range(n))), ''';
        TRUE : dest;
      esac;
    next(inside) :=
      case
        atFloor = floor & doorOpen[floor] & !inside & !(floor = dest) : TRUE;
        atFloor = dest & doorOpen[dest] & inside : FALSE;
        TRUE : inside;
      esac;''')

print(thing)