#!/usr/bin/perl -w

#calculation script CalcS for one construct

#TBD  Get rid of dec15 ?
use dec15;

$realeps = &dec15::geteps();
$eps = $realeps;  #larger than actual float granularity 

#phony use of some variables created in processing ccf files --- remove TBD?
$LBst2=0;$UBst2=0;$insubcount2=0;$valIntcpt0=0;$initialState2=0;$runSlope0=0;
$stsubcount0=0;$UBin0=0;$LBin0=0;$LBst0=0;$UBst0=0;$initialState0=0;

sub warnmess{ #print warning based on V option
  unless ($Voption && defined($_[0])) {return;}
  $mess = "";
  MLOOP: for ($wm=0;;$wm++) {
    unless (defined($_[$wm])) {last MLOOP;}
    $mess = $mess.$_[$wm];
  }
warn $mess, "\n";
}

#get options passed by SYNS
$Voption = 0;  #default is silent
$allOptions = "";
OPT: for ($i = 0;;$i++) { #over all options
  unless (defined($ARGV[$i])) {last OPT;}
  $allOptions = $allOptions." ".$ARGV[$i];
  if ($ARGV[$i] eq "-V") {
    $Voption = 1;
  }
}
$thecurrentflag = "L"; #to mark the output theory files
$Rely = 0; # global may be set in the process_ccf subroutine

#########################################
#   read controling file system.sscf
#########################################
$i = 0;
open(SSCF, "system.sscf") or die "Control file system.sscf missing";
chop($type = <SSCF>);
#debug
#print "|$type|\n";
if($type eq "conditional" || $type eq "loop") {
  chop ($ccf0 = <SSCF>);
}
chop($ccf1 = <SSCF>);  #The TRUE branch for conditional
unless ($type eq "loop") {
  chop($ccf2 = <SSCF>);
}
close SSCF;

########################################################
#subroutine to read a .ccf[t|c] file and store in memory
#
sub store_ccf { #parameters:  .ccf file name, construct type
my ($ccfFile, $type);
my ($meas, $line, $paramline, $stateless, $ccftFile, $ccfcFile, $i);
my ($scount, $insubcount, @stsubcount);
  $ccfFile = $_[0]; 
#debug
#print "|$ccfFile|\n";
  $type = $_[1];
#debug
#print "ccf file: $ccfFile \n";
  @filePre = split(/\./,$ccfFile);
  $ext = $filePre[$#filePre];
  $ProgFile = $filePre[0];  # use parameter ccf file name w/o extension
#debug
#print "Program file: $ProgFile \n";
  open(CCF,$ccfFile) or die "no component control file ",$ccfFile;
  chop($paramline = <CCF>);
  unless ($paramline =~ /^theory/ || $ext eq "ccfc") { # .ccf is not actual component; no other files to read
    close(CCF);  #use the same filehandle
    $newFile = $ccfFile."t";
    open(CCF,"<$newFile") or die "component ",$ccfFile," has missing $newFile file";
    $paramline = <CCF>;  #get the control line to parallel .ccf case above
  } 
  @code = split(" ",$paramline);
  $stateless = 1;
  ${"scount".$type} = 0;
  if ($ext eq "ccfc" || (defined($code[2]) && ($code[2] eq "R" || $code[2] eq "N"))) {
    $stateless = 0; #lousy test for component with state...
    if ($ext ne "ccfc") { #must go deeper yet...
      close(CCF); #filehandle to be used again
#TBD check if t or c is newer and perhaps omit next
      system "./ccft2ccfc $ccfFile"; #create .ccfc file
      open(CCF,"<$ccfFile"."c") or die "no $ccfcFile file for component with state";
      $paramline = <CCF>;
    }
    @params = split(" ",$paramline);
    $scount = $params[1];
    ${"scount".$type} = $scount;
    $insubcount = $params[2];
    ${"insubcount".$type} = $insubcount;
    $totalstatesubd = 0;
    for ($i=0; $i<$scount; $i++) { #state counts
      $stsubcount[$i] = $params[3+$i];
      $totalstatesubd += $stsubcount[$i];
      ${"stsubcount".$type}[$i] = $stsubcount[$i];
    }
    for ($i=0; $i<$scount; $i++) { #initial state values
      ${"initialState".$type}[$i] = $params[3+$scount+$i];
    }
    ${"datastart".$type} = $insubcount + $totalstatesubd + 1; #count from 0 where first data item lies
    for ($i=0; $i<$insubcount; $i++) { #input subdomains
      $line = <CCF>;
      @data = split(" ",$line);
      ${"LBin".$type}[$i] = $data[0];
      ${"UBin".$type}[$i] = $data[1];
    }
    for ($sc=0; $sc<$scount; $sc++) {
      for ($i=0; $i<$stsubcount[$sc]; $i++) { #state subdomains
        $line = <CCF>;
        @data = split(" ",$line);
        ${"LBst".$type}[$sc][$i] = $data[0];
        ${"UBst".$type}[$sc][$i] = $data[1];
      }
    }
  }
  if (defined($code[3]) && $code[2] eq "r") { #reliability file
    $Rely = $code[3]; #set by any stateless file being "r", value is the confidence % >0
    #TBD for state case... more care for some set and some not
  }
  #one of three files positioned at start of data
  if ($type == 0) {
    $meas = \@range0;
  } elsif ($type == 1) {
    $meas = \@range1;
  } else { # must be 2
    $meas = \@range2;
  }
  unless ($stateless) {
    $inSidx = 0; #counters for the subdomain hash
    for ($i=0; $i<$scount; $i++) {
      $stSidx[$i] = 0;
    }
  }
  $i = 0;
  while ($line = <CCF>) {
    @data = split(" ",$line);
    if ($stateless) { # line is:  LB UB output-slope output-intercept runtime-slope runtime-intercept  
      ${"subDleft".$type}[$i] = $data[0];
      ${"LBin".$type}[$i] = $data[0];
      ${"subDright".$type}[$i] = $data[1];
      ${"UBin".$type}[$i] = $data[1];
      #TBD eliminate duplicate names when it's safe...
      if ($type == 0) { #conditional, force to 0/1
        $aveval = $data[2]*($data[0] + $data[1])/2.0 + $data[3];
        if ($aveval > -0.1 && $aveval < 0.3) {
          $compromise = 0;
        } elsif ($aveval >= 0.7 && $aveval < 1.3) {
          $compromise = 1;
        } else { #way off, quit
          die "for component ",$p0," test value ",$aveval, "on subdomain [",$line[0],", ",$line[1],") out of line";
        }
        unless (abs($aveval - $compromise) < 0.1) {  #had to fudge pretty badly
          warn "test component ",$ProgFile," does not have clear binary value on subdomain [",$line[0],", ",$line[1],
         ") -- $aveval replaced by $compromise";
        }
        ${"valSlope".$type}[$i] = 0;
        ${"valIntcpt".$type}[$i] = $compromise;
      } else { #not conditional test
        ${"valSlope".$type}[$i] = $data[2];
        ${"valIntcpt".$type}[$i] = $data[3];
      }
      ${"runSlope".$type}[$i] = $data[4];
      ${"runIntcpt".$type}[$i] = $data[5];
    } else { #with state--line (N states): inputLB inputUB N(statesLB UB) count output runtime N(resultstates)
      $statehash = "$inSidx";
      for ($j=0; $j<$scount; $j++) {
        $statehash .= " $stSidx[$j]";
      }

      if (++$inSidx >= $insubcount) {
        $inSidx = 0;
        BS:
        for ($s=0; $s<$scount; $s++ ) {
          if (++$stSidx[$s] >= $stsubcount[$s]) {
            $stSidx[$s] = 0;
          } else { #leave rest alone
            last BS;
          }
        }
      }

#debug:  list out the state order
#print "statehash: $statehash\n";
      ${"hits".$type}{$statehash} = $data[0];
      if ($type == 0) { #conditional, force to 0/1
        $aveval = $data[1];
        if ($aveval > -0.1 && $aveval < 0.3) {
          $compromise = 0;
        } elsif ($aveval >= 0.7 && $aveval < 1.3) {
          $compromise = 1;
        } else { #way off, quit
          #TBD print subdomain properly
          die "for component ",$p0," test value ",$aveval, "on subdomain [",$statehash,") out of line";
        }
        unless (abs($aveval - $compromise) < 0.1) {  #had to fudge pretty badly
          warn "test component ",$ProgFile," does not have clear binary value on subdomain [",$statehash,
         ") -- $aveval replaced by $compromise";
        }
        $data[1] = $compromise;
        $line = join(" ",@data);
      } 
      ${"output".$type}{$statehash} = $data[1];
      ${"runtime".$type}{$statehash} = $data[2];
      for ($s=0; $s<$scount; $s++) { #output state values
        ${"finalstate".$type}[$s]{$statehash} = $data[3+$s];
      }
    }
  chomp(@$meas[$i] = $line);
  $i++;
  }
  close(CCF);
  if ($stateless) { #set stuff missed above
    ${"insubcount".$type} = $i;
  }
  return $stateless, $ProgFile, $Rely; # parameters of the file (more TBD)
} #end of store_ccf subroutine
######################################################################


#the "rangex" arrays contain line strings for the subdomain intervals
#and must be split out to be used

#Test component is range0
if ($type eq "conditional" || $type eq "loop") {
  @params = store_ccf($ccf0,0);
  $range0cnt = scalar(@range0);
  $p0 = $params[1];
  $stateless0 = $params[0];
}

#range1 is 1st in series, TRUE for conditional, body for loop
@params = store_ccf($ccf1,1);
$range1cnt = scalar(@range1);
$p1 = $params[1];
$stateless1 = $params[0];
#debug
#foreach $h (%output1) { print "hash:$h; out:$output1{$h}; N:$hits1{$h}\n" if ($h =~ /\ /); }

#range2 is 2nd in series, FALSE for conditional
unless ($type eq "loop") {
  @params = store_ccf($ccf2,2);
  $range2cnt = scalar(@range2);
  $p2 = $params[1];
  $stateless2 = $params[0];
}
#debug
#foreach $h (%output2) { print "hash:$h; out:$output2{$h}; N:$hits2{$h}\n" if ($h =~/\ /); }

if ($Rely) { #some file was reliability, do that
  $thecurrentflag = "LC r $Rely";
}

##########################################
# component 0 is the test, if a conditional or loop
# component 1 first in a series, "true" part for conditional, body for a loop
# component 2 if a series or "false" part of conditional
##########################################


#################################################
# Subroutine definitions:
#
# take two intervals as arrays (left 0, right 1, left 2, right 3) 
#as input, and return # the intersection interval as a similar array.
# If the intersection is empty, return [1,0)
#

sub intersect { 
my(@int1,@int2,$t,@nul);
@nul = (1, 0);
@int1 = ($_[0], $_[1]);
@int2 = ($_[2], $_[3]);
#debug
#print "@int1\n";
#print "@int2\n";
# Make @int1 lie to the left
if ($int1[0] > $int2[0]) { 
  @int2 = ($_[0], $_[1]);
  @int1 = ($_[2], $_[3]);
}
if ($int1[0] < $int2[0]) { #strictly to the left
  if ($int1[1] <= $int2[0]) { #no intersection
    return @nul;
  }
  else {
    if ($int1[1] <= $int2[1]) { 
      return ($int2[0],$int1[1]);
    }
    else { #must be that 1 completely covers 2
      return ($int2[0],$int2[1]);
    }
  }
}
else { #left ends coincide
  if ($int1[1] <= $int2[1]) {$t = $int1[1];} else {$t = $int2[1];}
  return ($int1[0],$t);
}
}

##################################################
# test for empty interval
#   parameters are endpoints
sub notnull {
my($left, $right);
 $left = shift;
 $right = shift;
 #debug
 #print "empty? [$left $right)\n";
 if ($left >= $right) { return 0;  #empty
 }
 else { return 1;
 }
}
#####################################################

$theorytest = "once.ccf";
$theoryseries = "another.ccf";
$again = "again.ccf";
$theory = "theory.ccf";

$stateless3 = 1; #for all cases not state-ready yet

if ($type eq "conditional") {
  $stateall = $stateless0+$stateless1+$stateless2;
  $stateless3 = ($stateall == 3);
  if ($stateless3) {
    $k = 0; #counter for new subdomains created 
    $jstartT = 0;
    $jstartF = 0; #left-off indices for 2nd component subdomains
    for ($i=0; $i<$range0cnt; $i++) { #intersect subdomains
      $testTrue = $valIntcpt0[$i];
      $foundany = 0;
      if ($testTrue) {  # test is true on this subdomain
        $jstart = $jstartT;
        $jend = $range1cnt;
      } else {
        $jstart = $jstartF;
        $jend = $range2cnt;
      }
      IL: 
      for ($j=$jstart; $j<$jend; $j++) { # find any intersections with the proper component
        if ($testTrue) {
          @int = intersect(($subDleft0[$i],$subDright0[$i]),($subDleft1[$j],$subDright1[$j]));
          $TF = "TRUE";
          $runIntcpt = $runIntcpt1[$j];
          $runSlope = $runSlope1[$j];
          $valIntcpt = $valIntcpt1[$j];
          $valSlope = $valSlope1[$j];
        } else {
          @int = intersect(($subDleft0[$i],$subDright0[$i]),($subDleft2[$j],$subDright2[$j]));
          $TF = "FALSE";
          $runIntcpt = $runIntcpt2[$j];
          $runSlope = $runSlope2[$j];
          $valIntcpt = $valIntcpt2[$j];
          $valSlope = $valSlope2[$j];
        }
  #debug
  #print "@int \n";
        if (notnull(@int)) { #add to list of new subdomains
          $range3[$k] = "$int[0] $int[1] ";
          if ($Rely) { #reliability; just the intercept
            $thtimeSlope[$k] = 0;
            $thtimeIntcpt[$k] = $runIntcpt * $runIntcpt0[$i];
          } else {
            $thtimeSlope[$k] = $runSlope + $runSlope0[$i];
            $thtimeIntcpt[$k] = $runIntcpt + $runIntcpt0[$i];
          }
          $thvalSlope[$k] = $valSlope;
          $thvalIntcpt[$k] = $valIntcpt;
          $range3[$k] = $range3[$k] .dec15::dump15s($thvalSlope[$k]).dec15::dump15s($thvalIntcpt[$k])
             .dec15::dump15s($thtimeSlope[$k]).dec15::dump15s($thtimeIntcpt[$k]).$TF;
#debug
#print "Sls $k: $range3[$k]\n";
          $foundany = 1;
          $k++;
        } else { #null intersection
          if ($foundany) {
            if ($testTrue) {
              $jstartT = $j - 1;  #next time start where one was found
            } else {
              $jstartF = $j - 1;  
            }
            last IL;  #can't be any more this time
          }
        }
      } #end IL loop
    } #end loop over range0
    $range3cnt = $k;
  #end stateless3 case
  } else { #something has state
    $stateless3 = 0;
    $limit0 = $insubcount0;
    $limit0 = $range0cnt if ($stateless0);
    $limit1 = $insubcount1;
    $limit1 = $range1cnt if ($stateless1);
    $limit2 = $insubcount2;
    $limit2 = $range2cnt if ($stateless2);
    #intersect the THEN and ELSE input subdomains
    $jstart = 0;
    $limite = 0;  #count of intersections between then/else
    for ($i=0; $i<$limit1; $i++) {
    $foundany = 0;
      JL:
      for ($j=$jstart; $j<$limit2; $j++) {
        @intr = intersect(($LBin1[$i],$UBin1[$i]),($LBin2[$j],$UBin2[$j]));
        if (notnull(@intr)) {
#debug
#print "t/e $limite;$i,$j: $intr[0],$intr[1]\n";
          $thente[$limite] = $i;
          $elsete[$limite] = $j;
          $LBte[$limite] = $intr[0];
          $UBte[$limite++] = $intr[1];
          $foundany = 1;
        } else {
          if ($foundany) {
            $jstart = $j-1;
            last JL;
          }
        }
      } 
    }
    #intersect that intersection with the if-test subdomains
    $jstart = 0;
    $insubcount3 = 0;  #count of intersections between cond and then/else
    for ($i=0; $i<$limit0; $i++) {
      $foundany = 0;
      $thenMax[$i] = 0;
      $elseMax[$i] = 0;  #counters for indices added
      JLL:
      for ($j=$jstart; $j<$limite; $j++) {
        @intr = intersect(($LBin0[$i],$UBin0[$i]),($LBte[$j],$UBte[$j]));
        if (notnull(@intr)) {
#debug
#print "C $insubcount3: $thente[$j], $elsete[$j]; $intr[0],$intr[1]\n";
          $thendex[$i][$thenMax[$i]++] = $thente[$j];
          $elsedex[$i][$elseMax[$i]++] = $elsete[$j];
          $LBin3[$insubcount3] = $intr[0];
          $UBin3[$insubcount3++] = $intr[1];
          $foundany = 1;
        } else {
          if ($foundany) {
            $jstart = $j-1;
            last JLL;
          }
        }
      } 
    }
    $scount3 = $scount0 + $scount1 + $scount2;
    for ($i=0; $i<$scount0; $i++) {
      $stsubcount3[$i] = $stsubcount0[$i];
      $initialState3[$i] = $initialState0[$i];
      $LBst3[$i] = $LBst0[$i];
      $UBst3[$i] = $UBst0[$i];
    }
    for ($i=0; $i<$scount1; $i++) {
      $stsubcount3[$i+$scount0] = $stsubcount1[$i];
      $initialState3[$i+$scount0] = $initialState1[$i];
      $LBst3[$i+$scount0] = $LBst1[$i];
      $UBst3[$i+$scount0] = $UBst1[$i];
    }
    for ($i=0; $i<$scount2; $i++) {
      $stsubcount3[$i+$scount0+$scount1] = $stsubcount2[$i];
      $initialState3[$i+$scount0+$scount1] = $initialState2[$i];
      $LBst3[$i+$scount0+$scount1] = $LBst2[$i];
      $UBst3[$i+$scount0+$scount1] = $UBst2[$i];
    }

    $k = 0; #counter for @range3 structure
    $inj = 0; #cycle count for input subdomain of range0
    for ($j=0; $j<$range0cnt; $j++) { #loop over the conditional's inputs & states
      @newline = split(" ",$range0[$j]);
      if ($stateless0) {
        $TF = $valIntcpt0[$j];
        #put in state-form
        $x = ($newline[0] + $newline[1])/2; 
        $line[0] = 1; #phony non-zero count
        $line[1] = $valIntcpt0[$j];
        $line[2] = $newline[4]*$x + $newline[5]; #run time
        $newline = join(" ",@line); #eliminate rest of the line as garbage
      } else {
        $TF = $newline[1];
      }
      if ($TF) { #THEN component
        for ($qi=0; $qi<$thenMax[$inj]; $qi++) {
          $q = $thendex[$inj][$qi];
#debug
#print "r0: $j; qi: $qi, r1: $q\n";
          @newline = split(" ",$range0[$j]);
          $r0[$k] = $j;  #save index into range0
          $r1[$k] = $q;  #save initial index into range1
          @otherline = split(" ",$range1[$q]);
          if ($stateless1) { #shift to state format
            $x = ($otherline[0] + $otherline[1])/2;
            $otherline[0] = 1; #phony non-zero count
            $otherline[1] = $otherline[2]*$x + $otherline[3];
            $otherline[2] = $otherline[4]*$x + $otherline[5];
          }
          $newline[0] = $otherline[0] if ($newline[0]);  #count of hits
          $newline[1] = $otherline[1];  #state-format output and runtime
          $newline[2] += $otherline[2];
          for ($i=0; $i < $scount1; $i++) { #copy in THEN states
            $newline[3+$scount0+$i] = $otherline[3+$i];
          }
          for ($i=0; $i<$scount2; $i++) { #copy in ELSE states as identity
            $self = ($LBst2[$i][0] + $UBst2[$i][0])/2; # compute first value
            $newline[3+$scount0+$scount1+$i] = $self; #value of self-state
          }
          $newline[3+$scount0+$scount1+$scount2] = "TRUE";
          $line = join(" ",@newline);
          $range3[$k] = $line;
          $k++;
        } #end for 
      } else { #use ELSE component
        for ($qi=0; $qi<$elseMax[$inj]; $qi++) {
          $q = $elsedex[$inj][$qi];
#debug
#print "r0: $j; qi: $qi, r2: $q\n";
          @newline = split(" ",$range0[$j]);
          $r0[$k] = $j;
          $r2[$k] = $q;
          @otherline = split(" ",$range2[$q]);
          if ($stateless2) { #shift to state format
            $x = ($otherline[0] + $otherline[1])/2;
            $otherline[0] = 1; #phony non-zero count
            $otherline[1] = $otherline[2]*$x + $otherline[3];
            $otherline[2] = $otherline[4]*$x + $otherline[5];
          }
          $newline[0] = $otherline[0] if ($newline[0]);  #count of hits
          $newline[1] = $otherline[1];  #state-format output and runtime
          $newline[2] += $otherline[2];
          for ($i=0; $i<$scount1; $i++) { #copy in THEN states as identity
            $self = ($LBst1[$i][0] + $UBst1[$i][0])/2; # compute first value
            $newline[3+$scount0+$i] = $self;
          }
          for ($i=0; $i<$scount2; $i++) { #copy in ELSE states 
            $newline[3+$scount0+$scount1+$i] = $otherline[3+$i];
          }
          $newline[3+$scount0+$scount1+$scount2] = "FALSE";
          $line = join(" ",@newline);
          $range3[$k] = $line;
          $k++;
        } #end for
      }
      $inj = 0 if (++$inj >= $insubcount0);
    } #end loop over $range0
    $range3cnt = $k;
#debug
#foreach $l (@range3) {print "$l\n";}
    #range3 contains one complete cycle; must now duplicate and fix outputs for
    #  the states in the THEN/ELSE components
    $range3cnt0 = $range3cnt;
    $tfi = 3+$scount0+$scount1+$scount2;
    $N1 = 1;
    for ($i=0; $i<$scount1; $i++) {
      $N1 *= $stsubcount1[$i];
    }
    $k = $range3cnt; #place to continue in range3
    for ($ns1=1; $ns1<$N1; $ns1++) { #loop over range1
      for ($j=0; $j<$range3cnt0; $j++) { #loop over the existing range3
        @newline = split(" ",$range3[$j]);
        @original = split(" ",$range0[$r0[$j]]); #$r0 index saved from first pass thru range0
        $TF = ($newline[$tfi] eq "TRUE");
        if ($TF) { #THEN line; insert new values
          @otherline = split(" ",$range1[$ns1*$insubcount1+$r1[$j]]); #$r1 index from first pass
          $newline[0] = $original[0];
          $newline[0] = $otherline[0] if ($newline[0]);
          $newline[1] = $otherline[1];
          $newline[2] = $original[2] + $otherline[2];
          for ($i=0; $i<$scount1; $i++) {
            $newline[3+$scount0+$i] = $otherline[3+$i];
          }
        } else { # ELSE line:  insert new "identity" state for THEN 
          for ($i=0; $i<$scount1; $i++) {
            if ($i) { #not first
              $div *= $stsubcount1[$i-1];
            } else {
              $div = $insubcount1;
            }
            $s = $r2[$j] % $div; #state index at $r1[$j] in range1
            $self = ($LBst1[$i][$s] + $UBst1[$i][$s])/2;
            $newline[3+$scount0+$i] = $self;
          }
        }
        $range3[$k++] = join(" ",@newline);
      } #end loop over old range3
    } # end repetition loop over range1
    $range3cnt = $k;
    #range3 now has entries for all states of THEN; duplicate for ELSE
    $range3cnt1 = $range3cnt;
    $k = $range3cnt1; #start index for copying
    $N2 = 1;
    for ($i=0; $i<$scount2; $i++) {
      $N2 *= $stsubcount2[$i];
    }
    for ($ns2=1; $ns2<$N2; $ns2++) { #loop over range2
      $oj = 0;
      for ($j=0; $j<$range3cnt1; $j++) { #loop over the existing range3
        @line = split(" ",$range3[$j]);
        $TF = ($line[$tfi] eq "TRUE");
        if ($TF) { #THEN line; insert new "identity" state for ELSE parts
          for ($i=0; $i<$scount2; $i++) {
            if ($i) { #not first
              $div *= $stsubcount2[$i-1];
            } else {
              $div = $insubcount2;
            }
            $s = $r1[$j] % $div; #state index at $r1[$j] in range2
            $self = ($LBst2[$i][$s] + $UBst2[$i][$s])/2;
            $newline[3+$scount0+$scount1+$i] = $self;
          }
        } else { # ELSE line:  new values
#debug
#print "indices $j, $oj\n";
          @original = split(" ",$range0[$r0[$oj]]); #$r0, $r2 indices saved from first pass thru range0
          @otherline = split(" ",$range2[$ns2*$insubcount2+$r2[$oj]]);
          $newline[0] = $original[0];
          $newline[0] = $otherline[0] if ($newline[0]);
          $newline[1] = $otherline[1];
          $newline[2] = $original[2] + $otherline[2];
          for ($i=0; $i<$scount2; $i++) {
            $newline[3+$scount0+$scount1+$i] = $otherline[3+$i];
          }
        }
        $range3[$k++] = join(" ",@newline);
        $oj = 0 if (++$oj >= $range3cnt0); #confine $oj to original range0/3 size
      } #end loop over old range3
    } # end repetition loop over range1
    $range3cnt = $k;
    warn "Conditional synthesis involving state not well tested...";
  } #end state cases
}
elsif ($type eq "series") {
#########################################subroutines############################
#sub locateOutput { #compare serial & binary search
#$Serial = locateOutputS($_[0]);
#$Binary = locateOutputB($_[0]);
#if ($Serial != $Binary) {
  #warn "Searches disagreed: ", $Serial, " != ",$Binary;
#}
#return $Serial;
#}

#sub locateOutput{ #parameter is the point to locate in 2nd component domains
sub locateOutputS{ #parameter is the point to locate in 2nd component domains
 #return is the index in $LBin2/$UBin2 structures, or -1 if not found 
  my($find,$j);
  $find = $_[0];
#this has not been tested since changes for adding state...
  for ($j = 0; $j < scalar(@LBin2); $j++) { #serial search for now
    if ($find >= $LBin2[$j] && $find < $UBin2[$j]) { #found here
      return $j;
    }
  }
  return -1;
}

#sub locateOutputB{ #binary search version
sub locateOutput{ #binary search version
  my($needed,$L,$R,$j);
  $needed = $_[0];
  $L = 0;
  $R = $#LBin2;  #extremes of subscripts of intervals
  INNER: while (1) {  #must jump out
    #subdomains are in order and disjoint and cover the domain
    $j = int(($L + $R)/2);  #TBD could start at right fraction of interval
  #careful, must look at two intervals at the end
     # if two, then $j is $L to start
  #debug
  #$str = "binary search for ".$needed." in [".$L.",". $R ."], index: ".$j;
  #print "$str \n";
  #end debug
    if ($R - $L + 1 <= 2) { #must be in these subdomains if here
      #try first one
      #debug
      #printf "needed: %.18e in [%.18e,%.18e)\n", $needed, $LBin2[$j],$UBin2[$j];
      if ($needed >= $LBin2[$j] && $needed < $UBin2[$j]) { #found
        last INNER
      }
      if ($L != $R) { # there were two, try the other
        $j = $R;
      #debug
      #printf "needed: %.18e in [%.18e,%.18e)\n", $needed, $LBin2[$j],$UBin2[$j];
        if ($needed >= $LBin2[$j] && $needed < $UBin2[$j]) { #found
          last INNER
        }
      }
      #not in either one, so can't be found
      return -1;
    }
    else { # [L,R] more than two subdomains; which way to shift?
      if ($needed < $LBin2[$j]) { #it's left of here
        $R = $j;
      }
      else { #right
        $L = $j;
      }
    }
  } #end while(1)
  return $j;
} #end binary search version
#####################################################################################
  $stateless3 = 0;
  if ($stateless1 && $stateless2) {
    $stateless3 = 1;
    @rec0 = split(" ",$range2[0]);
    @reck = split(" ",$range2[$range2cnt-1]);
    $k = 0;  #accumulate new subdomains in $range3[$k]
    SUBD: for($i=0; $i<$range1cnt; $i++) { #over all first subdomains
      $begin1 = $subDleft1[$i];
      $end1 = $subDright1[$i];
      #1st component subdomain is [$begin1, $end1]
      if ($end1 < $begin1) { # should not happen
        die "interval [,",$begin1,", ",$end1,") reversed?";
      }
      #debug
      #print "Subd: [$begin1, $end1)\n";
      $slope = $valSlope1[$i];
      $intcpt = $valIntcpt1[$i];
      if (abs($slope) <= $eps) { #special case for faster step-function approx
        $thvalSlope[$k] = 0.0;
        $j = locateOutput($intcpt);
        if ($j < 0 ) { #not found
          warn "Functional value on subdomain [",$subDleft1[$i],", ",$subDright1[$i],") undefined because output $needed from ",$p1, " falls in no ",$p2," subdomain";
          $thvalIntcpt[$k] = 0; #phony value
          $thtimeSlope[$k] = 0;
          $thtimeIntcpt[$k] = -1; #"undefined!"
          $TF = "SERIES";
        } else {
          $thvalIntcpt[$k] = $valSlope2[$j]*$intcpt + $valIntcpt2[$j];
          if ($Rely) { #reliability; just the intercept
            $thtimeSlope[$k] = 0;
            $thtimeIntcpt[$k] = $runIntcpt2[$j] * $runIntcpt1[$i];
          } else {
            $thtimeSlope[$k] = $runSlope1[$i] + $slope*$runSlope2[$j];
            $thtimeIntcpt[$k] = $runSlope2[$j]*$intcpt + $runIntcpt2[$j] + $runIntcpt1[$i];
          }
          @check = split(" ",$range2[$j]);
          if (defined($check[6])) {
            $TF = $check[6];
          }
          else {
            $TF = "SERIES";
          }
        }
        #debug
        #print "$i/$j:$thvalIntcpt[$k]($TF) ";
        $range3[$k] = dec15::dump15s($subDleft1[$i]).dec15::dump15s($subDright1[$i]). dec15::dump15s($thvalSlope[$k]).dec15::dump15s($thvalIntcpt[$k]).dec15::dump15s($thtimeSlope[$k]).dec15::dump15s($thtimeIntcpt[$k]).$TF;

        $k++; #bump count of new intervals
        next SUBD; #done with 1st-comp subdomain
      } # end special case of zero slope
      #get here only if $slope != 0
      $L = 0;  # count of intervals into which this subdomain is broken
      $reltiny = &dec15::epsplace($end1 - $begin1); #float error relative to interval
      $left = $begin1;
      $lastj = -99; #the 2nd comp subdomain found on the previous time
      $sev = 1; #number of epsilons to ignore for float fuzz
      #$flag = 10; #see debug below
      SUBSUB: while ($left < $end1) { #jump out when all intervals obtained
        $diverge = 0; #assume the current interval will have a functional value
        #Assumes contiguous subdomains in 2nd component
        $needed = $slope*$left + $intcpt; 
        #debug
        #print "in: $left, out: $needed\n";
        $j = locateOutput($needed); 
        $inj = $j;  # save for adjusting below
        if ($left > $begin1 && $j == $lastj) {#found same 2nd-comp interval, must move on
          if ($slope > 0) {
            $j++;
          } else { # should really fix locateOutput to know about negative slopes...
            $j--; 
            $inj = $j; #so don't report it...
          }
        }
        @check = split(" ",$range2[$j]);
        #tiny subdomains sometimes created at beginning or end-- allow
        #if ($slope < 0 && abs($needed - $check[0]) <= $eps) {
        #  $j--;
        #}
        #if ($slope > 0 && abs($needed - $check[1]) <= $eps) {
        #  $j++;
        #}
        if (abs($j - $inj) > 0) { #did adjustment, OK?
          #debug and declare "flag" above
          #if ($flag-- > 0) { warn "adjust start from $inj to $j"; @check = split(" ",$range2[$inj]); warn "in (1)[",$begin1,", ",$end1,"), (2)[",$check[0],", ",$check[1],"): subdomain [",$left,", ? ); slope: ",$slope,"; value: ",$needed,"; count: ",$L; }
        }
          if ($j < 0 || $j >= $range2cnt) { #should also check if the proper endpoint in here
            $j = -1; #fake not found
          }
        if ($j < 0) { #not found
          if ($L) { #but some found already, so rest uncovered
            $right = $end1;
            warn "Functional value on subdomain [",$left,", ",$end1,") undefined because output $needed from ",$p1, " falls in no ",$p2," subdomain";
            $diverge = 1;
          } else {
            # not-found case if none found so far
            if ($slope > 0) { #reflect back the first interval start
              $right = ($rec0[0] - $intcpt)/$slope;
            } else { #slope negative, reflect back the last interval end
              $right = ($reck[1] - $intcpt)/$slope
            }
            if ($slope == 0 || $left > $end1 || $right <= $left) {
              $right = $end1;
            }
            #try again with next bit (if any), but this interval uncovered
            warn "Functional value on subdomain [",$begin1,", ",$right,") undefined because output $needed from ",$p1, " falls in no ",$p2," subdomain";
            $diverge = 1;
          }
            #continue below with "undefined" interval
        } else {# $left's output found at $j
          $jj = locateOutput($slope*$end1 +$intcpt);
          if ($jj == $j) { #same second-comp interval (covers slope 0 or almost 0 case)
            #whole interval retained
            $right = $end1;
          }
          #reflect back 2nd-component interval boundary to 1st domain
          elsif ($slope > 0) {
            $right = ($subDright2[$j] - $intcpt)/$slope; 
          }
          else { #slope < 0
            $right = ($subDleft2[$j] - $intcpt)/$slope;  #worry about open end?
          } #end slope cases  
          if ($right >= $end1) {
            $right = $end1;
          }
        } # end of the found case
        @check = split(" ",$range2[$j]); #get 2nd component values
        if ($right - $left <= $sev*$reltiny|| $right - $left <= $eps) {# tiny interval
          warnmess "in (1)[",$begin1,", ",$end1,"), (2)[",$check[0],", ",$check[1],"): tiny subdomain created [",$left,", ",$right,"); slope: ",$slope,"; value: ",$needed,"; count: ",$L;
            #$left = $right + $sev*&dec15::epsplace($right); #shift and omit this interval 
            #next SUBSUB; #fix when the theory file is written
        }
        if ($diverge) { #functional value undefined on this subdomain
          #mark by negative runtime 
          $thvalSlope[$k] = 0;
          $thvalIntcpt[$k] = 0; #phony values
          $thtimeSlope[$k] = 0;
          $thtimeIntcpt[$k] = -1;
        } else { #regular case
          if (defined($check[6])) {
            $TF = $check[6];
          }
          else {
            $TF = "SERIES";
          }
          $thvalSlope[$k] = $slope*$valSlope2[$j];
          $thvalIntcpt[$k] = $valSlope2[$j]*$intcpt + $valIntcpt2[$j];
          #if (abs($thvalSlope[$k]) > 1000 && $right - $left < .01*($reck[1] - $rec0[0])) { #change to constant!
          if ($end1-$begin1 < .001 && abs($thvalSlope[$k]) > 1000 && abs($thvalSlope[$k])*($right - $left)  > .3*($reck[1] - $rec0[0])) { #change to constant!
            warnmess "Made step-function interval [",$left,", ", $right,"), slope was ",$thvalSlope[$k];
            $thvalIntcpt[$k] = $thvalSlope[$k]*($right + $left)/2 + $thvalIntcpt[$k];
            $thvalSlope[$k] = 0;
          }
          if ($Rely) { #reliability; just the intercept
            $thtimeSlope[$k] = 0;
            $thtimeIntcpt[$k] = $runIntcpt2[$j] * $runIntcpt1[$i];
          } else {
            # run times: mx+b + m'x'+b', x' = output of C1 on input x
            $thtimeSlope[$k] = $runSlope1[$i] + $slope*$runSlope2[$j];
            $thtimeIntcpt[$k] = $runSlope2[$j]*$intcpt + $runIntcpt2[$j] + $runIntcpt1[$i];
          }
        } #end regular case
        $range3[$k] = dec15::dump15s($left).dec15::dump15s($right). dec15::dump15s($thvalSlope[$k]).dec15::dump15s($thvalIntcpt[$k]).dec15::dump15s($thtimeSlope[$k]).dec15::dump15s($thtimeIntcpt[$k]).$TF;

        #debug
        #print "$range3[$k] \n";
        $L++;
        $k++;
        if ($right >= $end1) { #test for done with covering this subdomain
          last SUBSUB;
        }
        $left = $right;
        $lastj = $j;
      } #end of SUBSUB loop
    }  # end for $i (first comp subdomain loop)
    $range3cnt = $k;
  } elsif (!$stateless1 && $stateless2) { #state;stateless
    #initial stuff same as 1st component
    $scount3 = $scount1;
    $insubcount3 = $insubcount1;
    for ($i=0; $i<$insubcount1; $i++) {
      $LBin3[$i] = $LBin1[$i];
      $UBin3[$i] = $UBin1[$i];
    }
    for ($i=0; $i<$scount1; $i++) {
      $initialState3[$i] = $initialState1[$i];
      $stsubcount3[$i] = $stsubcount1[$i];
      for ($j=0; $j<$stsubcount1[$i]; $j++) {
        $LBst3[$i][$j] = $LBst1[$i][$j];
        $UBst3[$i][$j] = $UBst1[$i][$j];
      }
    }
    #end initial stuff
    #adjust the 1st component outputs and run times
    $range3cnt = $range1cnt;
    for ($k=0; $k<$range1cnt; $k++) {
      $line = $range1[$k];
        @lane = split(" ",$line);
        if ($lane[0] > 0) { #need not consider infeasable subdomains
          #get the subdomain from the 2nd component
          $j = locateOutput($lane[1]);
          if ($j < 0 ) { #not found
            warn "Functional value on subdomain [?",
              #TBD print all input/state sub domains here...
              ") undefined because output $lane[1] from ",$p1, " falls in no ",$p2," subdomain";
            $lane[0] = 0; #nice way to go undefined!
          } else {
            $lane[1] = $valSlope2[$j]*$lane[1] + $valIntcpt2[$j]; #output changed
            $lane[2] += $runSlope2[$j]*$lane[1] + $runIntcpt2[$j]; #run time fixed
          }
          $line = join(" ",@lane);
        }
      $range3[$k] = $line;
    }
  } elsif ($stateless1 && !$stateless2) { #stateless;state
    #TBD use non-zero slope to intersect second subdomains (maybe never...)
    $k = 0; #counter for range3
    $saidonce = 0;
    $NinRep2 = 1; #number of repeats of input subdomain list in range2
    for ($i=0; $i < $scount2; $i++) {
      $NinRep2 *= $stsubcount2[$i];
    }
    $range3cnt = $range1cnt*$NinRep2;
    $scount3 = $scount2;
    $insubcount3 = $range1cnt;
    for ($i=0; $i<$insubcount3; $i++) {
      $LBin3[$i] = $LBin1[$i];
      $UBin3[$i] = $UBin1[$i];
    }
    for ($i=0; $i<$scount2; $i++) {
      $stsubcount3[$i] = $stsubcount2[$i];
      $initialState3[$i] = $initialState2[$i];
      $LBst3[$i] = $LBst2[$i];
      $UBst3[$i] = $UBst2[$i];
    }
    for ($ns2=0; $ns2<$NinRep2; $ns2++) {
      for ($i=0; $i<$range1cnt; $i++) { #loop over first comp inputs
        if ($valSlope1[$i] != 0 && !$saidonce) {
          warn "Series synthesis using stateless (linear) first component ",
            "reduced to step-function approximation";
          $saidonce = 1;
        }
        if ($ns2 == 0) { #first time over range1 inputs
          $aveout1 = $valSlope1[$i]*($LBin1[$i] + $UBin1[$i])/2 + $valIntcpt1[$i]; #step value
          $j = locateOutput($aveout1);
          if ($j < 0) {
            warn "Functional value on subdomain [",$LBin1[$i],",",$UBin1[$i],") undefined because output ",
               "$aveout1 from $p1 falls in no $p2 subdomain";
            $j2[$i] = "u"; #this input undefined
          } else { #found in second comp inputs (first repetition of inputs)
            $j2[$i] = $j;  #index where range1 out found in range2 input subds
          }
        } #end of first time lookups
        if ($j2[$i] eq "u") {
          $range3[$k] = "0"; #undefined:  hit count 0
          for ($s=0; $s < $scount2; $s++) {
            $range3[$k] .= " 0"; #add phony state
          }  
        } else { #defined; get the right input repetition from range2
          $j = $ns2*$insubcount2 + $j2[$i];
          @line = split(" ",$range2[$j]);
          $line[2] += $runSlope1[$i]*($LBin1[$i] + $UBin1[$i])/2 + $runIntcpt1[$i]; #add run times
          $range3[$k] = join(" ",@line);
#debug
#print "ins $i; outs $j2[$i]; 2nd: $j, $line[1]\n";
        }
        $k++;
      } #end for over range1 
    } #end for over range2 input repeats
  #This case could probably be combined with the more general one below TBD?
  } else { #both components have state
    #initial stuff -- union of the state subdomains
    $scount3 = $scount1 + $scount2;
    $insubcount3 = $insubcount1;
    for ($i=0; $i<$insubcount3; $i++) {
      $LBin3[$i] = $LBin1[$i];
      $UBin3[$i] = $UBin1[$i];
    }
    for ($i=0; $i<$scount1; $i++) {
      $initialState3[$i] = $initialState1[$i];
      $stsubcount3[$i] = $stsubcount1[$i];
      for ($j=0; $j<$stsubcount1[$i]; $j++) {
        $LBst3[$i][$j] = $LBst1[$i][$j];
        $UBst3[$i][$j] = $UBst1[$i][$j];
      }
    }
    $ioff = $i;
    for ($i=0; $i<$scount2; $i++) {
      $initialState3[$ioff+$i] = $initialState2[$i];
      $stsubcount3[$ioff+$i] = $stsubcount2[$i];
      for ($j=0; $j<$stsubcount2[$i]; $j++) {
        $LBst3[$ioff+$i][$j] = $LBst2[$i][$j];
        $UBst3[$ioff+$i][$j] = $UBst2[$i][$j];
      }
    }
    #end initial stuff
    $range3cnt = $range1cnt;
    for ($i=0; $i<$scount2; $i++) {
      $range3cnt *= $stsubcount2[$i];
    }
    $k1 = 0;
    for ($i=0; $i<$scount2; $i++) { #state indices in 2nd component
      $ks[$i] = 0;
    }
    for ($k=0; $k<$range3cnt; $k++) {
      @data1 = split(" ", $range1[$k1]);
      if ($data1[0] > 0) { #don't do infeasible subdomains
        $out1 = $data1[1];
        $idex2 = locateOutput($out1);  #2nd comp input subdomain (first occurrence if several)
        if ($idex2 < 0) { # not found
          warn "Functional value on subdomain [?",
            #TBD print all input/state sub domains here...
            ") undefined because output $out1 from ",$p1, " falls in no ",$p2," subdomain";
          $data1[0] = 0; #nice way to go undefined!
        } else {
          $k2 = $idex2;
          for ($i=0; $i<$scount2; $i++) {
            $shft = 1;
            for ($j=0; $j<$i; $j++) {
              $shft *= $stsubcount2[$j];
            }
            $k2 += $shft*$insubcount2*$ks[$i];
          }
          @data2 = split(" ", $range2[$k2]);
          $data1[1] = $data2[1]; #change output
          $data1[2] += $data2[2];  #add to run time
          for ($i=0; $i<$scount2; $i++) {
            $data1[3+$scount1+$i] = $data2[3+$i];  #add additional states
          }
          if ($data2[0] == 0) { #second comp state infeasable
            $data1[0] = 0;
          }
        }
      } else { #append right number of zeroes
        for ($i=0; $i<$scount2; $i++) {
          $data1[3+$scount1+$i] = 0;
        }
      }
      $range3[$k] = join(" ",@data1);
      if (++$k1 >= $range1cnt) {
        $k1 = 0;
        #move to next state entry in $range2
        BS:
        for ($s=0; $s<$scount2; $s++ ) {
          if (++$ks[$s] >= $stsubcount2[$s]) {
            $ks[$s] = 0;
          } else { #leave rest alone
            last BS;
          }
        }
      }
    }
  }
}
elsif ($type eq "loop") {
  $stateless3 = ($stateless0+$stateless1==2);
warn "Synthesis of loops with state not tested" if ($stateless3);
  #create subdirectory, do single calculation there, and bring back to this
  # directory the computed "theory" file 
  $thidx = 0;
  $subdir = ".SubCalcLoop";  #name of the subdirectory
  `rm -r -f $subdir`; #destroy directory so it can be used repeatedly
  mkdir $subdir;
  `cp * $subdir`;  #copy needed files
  chdir $subdir; #shift to new directory
#debug -- where are we?
#print `pwd`;
  #build a proper .sscf file
  open (SSCF, ">system.sscf") || die "can't create .sscf file for calculation";
  if ($p1 =~ /^theory/) {
    @tmp = split(/\./,$ccf1);
    $p1 = $tmp[0];  #no "program" name, use file name w/o .ccf
  }
  $p2 = "(ident)";
  $Cfalse = "ident.ccft";
  $Ctrue = $ccf1;
  $Ctest = $ccf0;
  warnmess "  Conditional:  IF ",$p0," THEN ",$p1," ELSE ",$p2," FI -> once  -> again";
  print SSCF "conditional\n";
  print SSCF "$Ctest\n";
  print SSCF "$Ctrue\n";
  print SSCF "$Cfalse\n";
  close SSCF;
  $itf = 6;  
  $itf = 3+$scount0+$scount1 unless ($stateless3);
  #index where the "TRUE/FALSE" will be placed by conditional synthesis
#debug
#print `cat system.sscf`;
  if (-1 == system "./CalcF ".$allOptions) {die "`CalcF' script failed"} ;
  $cmd = "mv -f ".$theory." ../".$theorytest;
  `$cmd`;
  chdir ".."; #back to parent directory
  #debug 
  #system "cp $theorytest /tmp/looptest.ccf";

  # copy FALSE subdomains into "theory.ccf"
  #  and the TRUE subdomains into "again.ccf"
  open (THEO, $theorytest) || die "Can't open ", $theorytest;
  $tmp = <THEO>;  #skip first line (file name)
  open (THE, ">".$theory) || die "Can't open ",$theory;
  print THE "theory $thecurrentflag\n";
  open (AGAIN, ">".$again) || die "Can't open ",$again;
  print AGAIN "theory $thecurrentflag\n";
  $anytrue = 0;
  $totalsubs = 0;
  while ($line = <THEO>) {
    @isit = split(" ", $line);
    $totalsubs++;
      if ($isit[$itf] eq "TRUE")  {
        print AGAIN $line;
        $anytrue += 1;
      }
      else { #came out FALSE
        if ($isit[$itf] ne "FALSE") {
        `cat $theorytest`;
        print "T/F index: $itf\n";
        die "Non-Aristotlian!";
        }
        print THE $line;
      }
  }
  close(THEO);
  close(THE);
  close(AGAIN);
  $anytrue1 = $anytrue; #to compare number of subdomains still true after one unwinding
  if ($anytrue) {
    warnmess "  (`again' is stripped of false subdomains -- ",$anytrue,"/",$totalsubs," active)";
    $againame = $again."0";
    system "cat $again > /tmp/$againame";
  }

  FL:
  while ($anytrue) { #not all the subdomains came out FALSE
    #check for unending theory loop
    open(ONE,">again1");
    open(AGAIN,$again);
    $tmp = <AGAIN>; #discard name
    while ($line = <AGAIN>) { #copy line
      print ONE $line;
    }
    close(ONE);
    close(AGAIN);
  
    #create subdirectory, do calculation there, and bring back the result
    $subdir = ".SubCalcLoop";  #name of the subdirectory
    `rm -r -f $subdir`; #destroy directory so it can be used repeatedly
    mkdir $subdir;
    `cp * $subdir`;  #copy needed files
    chdir $subdir; #shift to new directory
  #debug -- where are we?
  #print `pwd`;
    #build a proper .sscf file
    open (SSCF, ">system.sscf") || die "can't create .sscf file for calculation";
    #$p1 = "again";
    #$p2 = "theorytest";
    print SSCF "series\n";
    print SSCF "$again \n";
    print SSCF "$theorytest \n";
    close SSCF;
  #debug
  #print `cat system.sscf`;
  #system "cat $again"; system "cat $theorytest"; die "stop.";
    if (-1 == system "./CalcF ".$allOptions) {die "`CalcF' script failed"} ;
    $cmd = "mv -f ".$theory." ../".$theoryseries;
    `$cmd`;
    chdir ".."; #back to parent directory
  
    #copy FALSE subdomains into "theory.ccf", TRUE into "again.ccf"
    #check if all subdomains have taken FALSE branch
  
    open (THEO, $theoryseries) || die "can't open $theoryseries";
    $tmp = <THEO>;  #skip first line (file name)
    open (THE, ">>".$theory) || die "can't append to $theory";
    open (AGAIN, ">".$again) || die "can't open $again";
    print AGAIN "theory $thecurrentflag\n";
    $anytrue = 0;
    while ($line = <THEO>) {
      @isit = split(" ", $line);
        if ($isit[$itf] eq "TRUE")  {
          print AGAIN $line;
          $anytrue += 1;
        }
        else { #came out FALSE
          if ($isit[$itf] ne "FALSE") {
            `cat $theorytest`;
            print "T/F index: $itf\n";
            die "Non-Aristotlian!";
          }
          print THE $line;
        }
    }
    close(THEO);
    close(THE);
    close(AGAIN);
    #check for non-termination
    if ($anytrue == $anytrue1) { #no subdomain eliminated
      # not sure if this algorithm is correct for stateless piecewise-linear
      # it is NOT correct for state...  TBD
        if ($stateless3) {
          open(AGAIN,$again);
          $aga = <AGAIN>; #skip name
          open (ONE,"again1"); 
          CMPE: while (1) {
            $one = <ONE>;
            $aga = <AGAIN>;
            unless ($one) {last CMPE;}
            @part1 = split(" ",$one);
            @part2 = split(" ",$aga);
            if ($part1[0] != $part2[0] || $part1[1] != $part2[1]) { #subdomain differs
              #false alarm, keep going
              #debug
              #print "$one\n"; print "$aga \n";
              last CMPE;
            }
          }
        } else { #state:  fix TBD
          $one = 1;
        }
        unless ($one) { #exited loop at end, same subdomains
          die "  Loop calculation will never terminate";
        }
        close(AGAIN);
        close(ONE);
    }
    $thidx++;
    #debug 
    #$theoryname = $theory.$thidx; system "cp $theory /tmp/$theoryname";

    #sort the theory.ccf file in place  -- surely there must be a better way?!
    open(CCF,$theory);
    open (T1,">t1");
    $tmp = <CCF>;
    print T1 $tmp;
    close(T1);
    open (T2,">t2");
    while ($tmp = <CCF>) {
      print T2 $tmp;
    }
    close(T2);
    close(CCF);
    `rm -f $theory`;
    `cp t1 $theory`;
    `sort -g t2 >> $theory`;
    if ($anytrue) {
      warnmess "  Series: again;once  -> again ",$anytrue," subdomains still active";
      $anytrue1 = $anytrue; #ready for next iteration
      system "rm -f again1";
      system "cp $again again1";
      #debug 
      #$againdex++; $againame = $again.$againdex; `cp $again /tmp/$againame`;
    }
    else {
      warnmess "  Series: again;once -> again, termination";
    }
  } #end loop over $anytrue
}
else { 
  die "Construct type ", $type, " not implemented";
}

####################################################
#  create "theory" .ccf[c] file of results 
####################################################

if ($stateless3) { #result has no state, file is .ccf "theory"
unless ($type eq "loop") {  #stateless loop file already written above
# write the "theory" equivalent file
  open(TCCF, ">theory.ccf") || die "Could not write `theory' file";
  print TCCF "theory $thecurrentflag\n";
  #if ($type eq "conditional") {
    #@t1 = @t2 = ();
    #@range3 = sort {(@t1=split(" ",$a))[0] <=> (@t2=split(" ",$b))[0]} @range3;
  #} #else is "series," already sorted
  #sort is not needed... watch out if caught below for non-contiguous
  $R = -99; #phony value to start
  K3:
  for($k=0; $k<$range3cnt; $k++) { #check for contiguous as we go
    $lastR = $R; 
    @rline = split(" ",$range3[$k]);
    $L = $rline[0];
    $R = $rline[1]; #subdomain [L,R)
    if ($k > 0 && $lastR != $L && $p1.".ccf" ne $again) { #not contiguous, fix
      # but not if we are doing a loop, OK there
      warnmess "Gap ",$lastR,") [",$L," in ",$type," subdomains\n";
      $rline[0] = $lastR;
      $fixed = "";
      $kk = 0;
      while (defined($rline[$kk])) {
        $fixed = $fixed.$rline[$kk++]." "; 
      }
      $range3[$k] = $fixed;
    }
    @rline = split(" ",$range3[$k]);
    if ($rline[1] - $rline[0] <= $eps) {warn "Empty interval [",$rline[0],", ".$rline[1],") dropped\n"; next K3; }
    print TCCF "$range3[$k] \n";
  }
  close(TCCF);
}
} else { #result is a .ccfc "theory" file with state
  open(TCCF,">theory.ccfc") || die "Could not write `theory' file";
  print TCCF "theory $scount3 $insubcount3";
  for ($i=0; $i<$scount3; $i++) {
    print TCCF " $stsubcount3[$i]";
  }
  for ($i=0; $i<$scount3; $i++) {
    print TCCF " $initialState3[$i]";
  }
  print TCCF "\n";
  for ($i=0; $i<$insubcount3; $i++) {
    print TCCF "$LBin3[$i] $UBin3[$i]\n";
  }
  for ($i=0; $i<$scount3; $i++) {
    for ($j=0; $j<$stsubcount3[$i]; $j++) {
      print TCCF "$LBst3[$i][$j] $UBst3[$i][$j]\n";
    }
  }
  for ($k=0; $k<$range3cnt; $k++) {
    print TCCF "$range3[$k]\n";
  }
  close(TCCF);
}

