/*
  File: bisim.cc
  Author: Sudarshan S. Chawathe <chaw@cs.umd.edu>
  Date: 05th March, 2001
  Compile using: gcc -Wall -o bisim bisim.cc 
  Terms: GPL

  For the Maryland High School Programming Contest, 2001

  bisim: A (very) quick-and-dirty implementation of Bisimulation
  Copyright (C) 2001 Sudarshan S. Chawathe

  For details, see the accompanying bisim.ps file and any standard
  reference for bisimulation.  In particular, for an efficient
  algorithm *not* implemented here, see Robert Paige and Robert
  E. Tarjan. Three partition refinement algorithms. SIAM Journal on
  Computing, 16(6):973-989, December 1987.  What is implemented here
  is an inefficient hack suitable for a programming contest (only)!
   
  This program is free software; you can redistribute it and/or
  modify it under the terms of the GNU General Public License
  as published by the Free Software Foundation; either version 2
  of the License, or (at your option) any later version.
     
  This program is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  GNU General Public License for more details.
     
  You should have received a copy of the GNU General Public License
  along with this program; if not, write to the Free Software
  Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.  */

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <ctype.h>
#include <assert.h>

#define MAX_STR_LEN 32
#define MAX_NODES 64
#define MAX_DEG 16
#define MAX_LAB_LEN 32

#define MAX(a,b) ((a) > (b) ? (a) : (b))

int debug = 0;

typedef struct {
  char v[MAX_LAB_LEN];                   /* node label = "value" */
  int n;                                 /* number of edges */
  char l[MAX_DEG][MAX_LAB_LEN];          /* edge labels */
  int d[MAX_DEG];                        /* edge destinations */
} NodeInfo;

typedef NodeInfo Graph[MAX_NODES]; 

typedef short Grid[MAX_NODES][MAX_NODES];
/* Grid[x][y] nonzero means node x in graph 1 is (currently) similar to 
   node y in graph 2. */

void error(char * s)
{
  puts(s);
  exit(-1);
}

void dumpGraph(Graph G, int n)
{
  if(debug) printf("dumpGraph: node-id (label): edges as (label, dest)\n");
  for(int i = 0; i < n; i++) {
    printf("%d (%s):", i, G[i].v);
    for(int e = 0; e < G[i].n; e++) {
      printf(" (%s, %d)", G[i].l[e], G[i].d[e]);
    }
    printf("\n");
  }
}

int isEdge(Grid bisim, int n1, int n2, Graph G1, Graph G2, 
	   int s, char *l, int d, int rev)
  /* returns true iff G2 has an l-labeled edge from s to a node that is 
     sim to node d in G1; rev => roles of G1 and G2 are reversed in bisim */
{
  for(int e = 0; e < G2[s].n; e++) {
    /* is e the edge we need? */
    if(!strcmp(G2[s].l[e], l) && 
       (rev ? bisim[G2[s].d[e]][d] : bisim[d][G2[s].d[e]])) return 1;
  }
  if(debug) printf("isEdge: returning false for (%d, %s, %d)\n",
		   s, l, d);
  return 0;
}

int checkEdges(int x, int y, int n1, int n2, Graph G1, Graph G2, Grid bisim, 
	       int rev)
  /* returns true iff no edge out of node x violates the bisimilation;
   rev means the sense of G1 and G2 in bisim is reversed. */
{
  for(int e = 0; e < G1[x].n; e++) 
    if(!isEdge(bisim, n1, n2, G1, G2, y, G1[x].l[e], G1[x].d[e], rev)) return 0;
  return 1;
}

void getBisim(int n1, int n2, Graph G1, Graph G2, Grid bisim)
{
  /* initialize: all nodes in graph1 are similar to all nodes in graph2; 
     except for roots (node 0), which are only similar to the other root;
     and except when labels don't match */
  bisim[0][0] = 1;
  for(int i = 1; i < n1; i++) bisim[i][0] = 0;
  for(int j = 1; j < n2; j++) bisim[0][j] = 0;
  for(int i = 1; i < n1; i++) 
    for(int j = 1; j < n2; j++) 
      if(!strcmp(G1[i].v,G2[j].v)) bisim[i][j]=1;
  
  /* find and remove violations of the bisimulation condition: each
     edge out of a node must have a corresponding edge out of every
     node that is similar to it; corresponding means having same label
     and going to a node that is similar to the target of the edge
     from the first node */
  for(short change = 1; change; /* null */) {
    change = 0;
    for(int i = 0; i < n1; i++) {
      for(int j = 0; j < n2; j++) {
	if(bisim[i][j]) {
	  /* Can this pair of nodes continue to be similar? 
	     Check the condition on edges from both sides. */
	  if(!checkEdges(i, j, n1, n2, G1, G2, bisim, 0) ||
	     !checkEdges(j, i, n2, n1, G2, G1, bisim, 1)) {
	    change = 1;
	    bisim[i][j] = 0;
	    if(debug) printf("getBisim: Removing (%d, %d)\n", i, j);
	  };
	}
      }
    }
  }
}

int main(int argc, char * argv[])
{
  if(argc > 1) {
    debug = 1;
    printf("%s running in debugging mode...\n", argv[0]);
  }

  char instr[MAX_STR_LEN];
  int n1 = 0; 
  int n2 = 0;
  int s, d;
  Graph G1, G2;

  /* read in the edge-sets of two graphs */
  if(debug) printf("Reading first graph:\n"); 
  for(;;) { 
    scanf("%s", instr); if(!strncmp(instr,".", 2)) break;
    if(2 != scanf("%d %d", &s, &d)) error("Input format error");
    if(debug) printf("Read edge (%d, %s, %d)\n", s, instr, d); 
    {
      /* initialize the structures beyond those already init'd */
      int newN = MAX(s,d)+1;
      if(debug) printf("n1: %d, newN: %d\n", n1, newN);
      for(int i = n1+1; i < newN; i++) {
	G1[i].n = 0;
	G1[i].v[0] = '\0';
      }
      n1 = MAX(n1,newN);
    }
    G1[s].d[G1[s].n] = d;
    strcpy(G1[s].l[G1[s].n], instr);
    G1[s].n++;
  } 
  for(;;) {
    int node;
    scanf("%s", instr); if(!strncmp(instr,".", 2)) break;
    if(1 != scanf("%d", &node)) error("Input format error");
    if(debug) printf("(ni: %d) node %d: label %s\n", n1, node, instr);
    if(node >= n1) error("Input format error");
    strcpy(G1[node].v, instr);
  }
  if(debug) dumpGraph(G1, n1);

  if(debug) printf("Reading second graph:\n"); 
  for(;;) { 
    scanf("%s", instr); if(!strncmp(instr,".", 2)) break;
    if(2 != scanf("%d %d", &s, &d)) error("Input format error");
    if(debug) printf("Read edge (%d, %s, %d)\n", s, instr, d); 
    {
      /* initialize the structures beyond those already init'd */
      int newN = MAX(s,d)+1;
      for(int i = n2+1; i < newN; i++) {
	G2[i].n = 0;
	G2[i].v[0] = '\0';
      }
      n2 = MAX(n2,newN);
    }
    G2[s].d[G2[s].n] = d;
    strcpy(G2[s].l[G2[s].n], instr);
    G2[s].n++;
  } 
  for(;;) {
    int node;
    scanf("%s", instr); if(!strncmp(instr,".", 2)) break;
    if(1 != scanf("%d", &node)) error("Input format error");
    if(debug) printf("(ni: %d) node %d: label %s\n", n2, node, instr);
    if(node >= n2) error("Input format error");
    strcpy(G2[node].v, instr);
  }
  if(debug) dumpGraph(G2, n2);

  /* compute and print bisimulation */
  Grid bisim;
  getBisim(n1, n2, G1, G2, bisim);
  if(bisim[0][0] == 0) {
    printf("Glitch\n");
  }
  else {
    printf("No glitch\n");
    if(debug) {
      for(int i = 0; i < n1; i++) {
	printf("%d:", i);
	for(int j = 0; j < n2; j++) {
	  if(bisim[i][j] != 0) printf(" %d", j);
	}
	printf("\n");
      }
    }
  }
  return 0;
}