#!/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 
#debug
#print "$eps\n"; die "stopped";

#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];
  @filePre = split(/\./,$ccfFile);
  $ext = $filePre[$#filePre];
  $ProgFile = $filePre[0];  # use parameter ccf file name w/o extension
#debug
#print "Program file: $ProgFile ; Ext: |$ext|\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];
      }
    }
  }
#debug
#print "stateless = $stateless\n";
  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.5) {
          $compromise = 0;
        } elsif ($aveval >= 0.5 && $aveval < 1.1) {
          $compromise = 1;
        } else { #way off, quit
          die "for component ",$ProgFile," test value ",$aveval, "on subdomain [",$data[0],", ",$data[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;
        B1S:
        for ($s=0; $s<$scount; $s++ ) {
          if (++$stSidx[$s] >= $stsubcount[$s]) {
            $stSidx[$s] = 0;
          } else { #leave rest alone
            last B1S;
          }
        }
      }

#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.5) {
          $compromise = 0;
        } elsif ($aveval >= 0.5 && $aveval < 1.1) {
          $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;
 }
}
#####################################################

$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
#debug
#print "test: $line[2]\n";
        $range0[$j] = join(" ",@line); #eliminate rest of the line as garbage
        # this line of range0 is in the "state" format even tho stateless0 ...
      } else {
        $TF = $newline[1];
      }
      if ($TF) { #THEN component
        for ($qi=0; $qi<$thenMax[$inj]; $qi++) {
          $q = $thendex[$inj][$qi];
          $qq = $elsedex[$inj][$qi];
#debug
#print "r0: $j; qi: $qi, r1: $q\n";
          @newline = split(" ",$range0[$j]);
          $r0[$k] = $j; #index into range0
          $r1[$k] = $q;  #save initial index into range1
          $r2[$k] = $qq;  #index into range2
#debug
#print "THEN line: $range1[$q]\n";
          @otherline = split(" ",$range1[$q]);
          if ($stateless1) { #shift to state format
            if ($p1 eq "ident") {
              $otherline[0] = 1;
              $otherline[1] = ($LBin0[$inj] + $UBin0[$inj])/2;
              $otherline[2] = 0;
            } else {
              $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];
            }
          }
#debug
#print "then: $otherline[2]\n";
          @anotherline = split(" ",$range2[$qq]);
#         if ($stateless2 || $anotherline[0]) {
            $newline[0] = $otherline[0] if ($newline[0]);  #count of hits
#         } else {
#           $newline[0] = 0; #ELSE state infeasible, so omit (#not so!)
#         }
          $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
          }
          $nllast = 3+$scount0+$scount1+$scount2;
          $newline[$nllast] = "TRUE";
          $#newline = $nllast;
#debug
#print "sum: $newline[2]\n";
          $line = join(" ",@newline);
          $range3[$k] = $line;
          $k++;
        } #end for 
      } else { #use ELSE component
        for ($qi=0; $qi<$elseMax[$inj]; $qi++) {
          $q = $elsedex[$inj][$qi];
          $qq = $thendex[$inj][$qi];
#debug
#print "r0: $j; qi: $qi, r2: $q\n";
          @newline = split(" ",$range0[$j]);
#debug
#print "@newline\n";
          $r0[$k] = $j;
          $r1[$k] = $qq;
          $r2[$k] = $q;
          @otherline = split(" ",$range2[$q]);
          if ($stateless2) { #shift to state format
            if ($p2 eq "ident") {
              $otherline[0] = 1;
              $otherline[1] = ($LBin0[$inj] + $UBin0[$inj])/2;
              $otherline[2] = 0;
            } else {
              $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];
            }
          }
          @anotherline = split(" ",$range1[$qq]);
#         if ($stateless1 || $anotherline[0]) {
            $newline[0] = $otherline[0] if ($newline[0]);  #count of hits
#         } else {
#           $newline[0] = 0; #THEN state infeasible, so omit  ##(wrong!)
#         }
          $newline[1] = $otherline[1];  #state-format output and runtime
          $newline[2] += $otherline[2];
#debug
#print "else: $otherline[2]\n";
          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];
          }
          $nllast = 3+$scount0+$scount1+$scount2;
          $newline[$nllast] = "FALSE";
          $#newline = $nllast;
#debug
#print "sum: $newline[2]\n";
          $line = join(" ",@newline);
          $range3[$k] = $line;
          $k++;
        } #end for
      }
      $inj = 0 if (++$inj >= $insubcount0);
    } #end loop over $range0
    $range3cnt = $k;
#debug
#print "1st cycle:\n";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];
      $curst[$i] = 0;  #current state at this dimension
    }
    $curst[0] = 1;
    $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]);
#debug
#if (!defined($r0[$j])) {print "idx0: $j\n";}
        @original = split(" ",$range0[$r0[$j]]); #$r0 index saved from first pass thru range0
        @otherline = split(" ",$range1[$ns1*$insubcount1+$r1[$j]]); #$r1 index from first pass
        $TF = ($newline[$tfi] eq "TRUE");
        if ($TF) { #THEN line; insert new values
          $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" value for THEN state
          for ($i=0; $i<$scount1; $i++) {
            $s = $curst[$i]; #state index in range1
#debug
#print "cyc1idx: $j; stidx: $i; stsubidx: $s\n";
            $self = ($LBst1[$i][$s] + $UBst1[$i][$s])/2;
            $newline[3+$scount0+$i] = $self;
          }
          #r1 state is the first one for this pass, check for infeasible
          if (!$stateless2 && !$otherline[0]) {
            $newline[0] = 0;
          }
        }
        $range3[$k++] = join(" ",@newline);
      } #end loop over old range3
      $carry = 1;
      for ($i=0; $i<$scount1; $i++) { #update current state values
        if ($carry) {
          if ($curst[$i]+1 >= $stsubcount1[$i]) {
            $curst[$i] = 0;
          } else {
            $curst[$i]++;
            $carry = 0
          }
        }
      }
    } # end repetition loop over range1
    $range3cnt = $k;
#debug
#print "2nd cycle:\n"; foreach $l (@range3) {print "$l\n";}
    #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];
      $curst[$i] = 0;  #current state at this dimension
    }
    $curst[0] = 1;
    for ($ns2=1; $ns2<$N2; $ns2++) { #loop over range2
      $oj = 0;
      for ($j=0; $j<$range3cnt1; $j++) { #loop over the existing range3
        @newline = split(" ",$range3[$j]);
        @otherline = split(" ",$range2[$ns2*$insubcount2+$r2[$oj]]);
        $TF = ($newline[$tfi] eq "TRUE");
        if ($TF) { #THEN line; insert new "identity" state for ELSE parts
          for ($i=0; $i<$scount2; $i++) {
            $s = $curst[$i]; #state index  in range2
            $self = ($LBst2[$i][$s] + $UBst2[$i][$s])/2;
            $newline[3+$scount0+$scount1+$i] = $self;
          }
          if (!$stateless2 && !$otherline[0]) {
            $newline[0] = 0;
          }
        } else { # ELSE line:  new values
#debug
#print "indices $j, $oj, $r0[$oj], $r2[$oj]\n";
          @original = split(" ",$range0[$r0[$oj]]); #$r0 index saved from first pass thru range0
          $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);
        if (++$oj >= $range3cnt0) { #next block of inputs in r3
          $oj = 0; #confine $oj to original range0/3 size
        }
      } #end loop over old range3
      $carry = 1;
      for ($i=0; $i<$scount2; $i++) { #update current state values
        if ($carry) {
          if ($curst[$i]+1 >= $stsubcount2[$i]) {
            $curst[$i] = 0;
          } else {
            $curst[$i]++;
            $carry = 0
          }
        }
      }
    } # end repetition loop over range2
    $range3cnt = $k;
#debug
#print "3rd cycle:\n"; foreach $l (@range3) {print "$l\n";}
    warn "Conditional synthesis involving state not well tested...";
  } #end state cases
}
elsif ($type eq "series" || $type eq "compose") { 
 # "compose" does not cross-product states
 #   it is used for loop synthesis

#########################################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 locateStatesS{ #only serial search so far...TBD
sub locateStates{
 #input is a state and its number, output the subdomain index or -1 if not found
  my($states,$find,$i,$j,$n);
  $find = $_[0];
  $i = $_[1];
#debug
#print "to find:  state #$i, value $find\n";
  for ($j=0; $j<scalar($LBst2[$i]); $j++) {
    if ($find>=$LBst2[$i][$j] && $find<$UBst2[$i][$j]) { #found
#debug
#print "Found: $j\n"; 
      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";
    if ($R - $L + 1 <= 2) { #must be in these subdomains if here
#debug
#if ($L != $R) {print "Found $L/$R...\n";}
      #try second one first
      $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
      }
      if ($L != $R) { # there were two, try the other
        $j = $L;
      #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) { #"compose" is the same in the stateless case
    $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"; die "top of series";
      $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
      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++;
          } elsif ($slope < 0) { # should really fix locateOutput to know about negative slopes...
            $j--; 
          }
        }
        @check = split(" ",$range2[$j]);
        if ($slope < 0 && abs($needed - $check[0]) <= $eps) {
          $j--;
        }
        # enable code below to avoid a tiny interval
        #if ($slope > 0 && abs($needed - $check[1]) <= $eps) {
          #$j++;
        #}
        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
#debug 
#@check2 = split(" ",$range2[$inj]); if (abs($j - $inj) > 0) { warn "adjust start from $inj to $j"; warn "in (1)[",$begin1,", ",$end1,"), (2)[$check2[0],$check2[1]) & [$check[0],$check[1]): subdomain [$left, $right); slope: ",$slope,"; value: ",$needed,"; count: ",$L; } 

        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;
            #enable next code to omit
            #$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
    # "compose" same as series
    #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
            $lane[2] *= $runIntcpt2[$j] if ($Rely); #reliability
          }
          unless (defined($lane[3+$scount1])) { #TRUE/FALSE/SERIES slot
            $lane[3+$scount1] = "SERIES";
          }
          $line = join(" ",@lane);
        }
      $range3[$k] = $line;
    }
  } elsif ($stateless1 && !$stateless2) { #stateless;state
    #Not sure what "compose" means; will not arise with loops
    #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 0 0"; #undefined:  hit count 0, also output and runtime
          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
          @line1 = split(" ",$range1[$i]);
          if (defined($line1[6] )) { # add the TRUE/FALSE/SERIES mark
            $line[3+$scount2] = $line1[6];
          } else {
            $line[3+$scount2] = "SERIES";
          }
          $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;
    $scount3 += $scount2 if ($type ne "compose"); # "compose keeps first states only
    $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];
      }
    }
    if ($type ne "compose") {
      $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;
    if ($type ne "compose") {
      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 (defined($data1[3+$scount1])) { #TRUE/FALSE/SERIES slot
        $TF = $data1[3+$scount1];
      } else {
        $TF = "SERIES";
      }
      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;
          if ($type eq "compose") { #find the 2nd comp state
              $shft = 0;
            for ($i=0; $i<$scount2; $i++) {
              $needed = $data1[3+$i]; #state value
              $j = locateStates($needed,$i);
                if ($j<0) { # not found
                  die "State idex ",$i,", value $needed not found in $p2 subdomains";
                } else {
                  $blk = 1;
                  for ($jj=0; $jj<$i; $jj++) { #accumulate multiplier
                    $blk *= $stsubcount2[$jj];
                  }
                  $shft += $j*$blk;
                }
            } #end loop over statecount
              $k2 += $shft*$insubcount2;
          } else {
            for ($i=0; $i<$scount2; $i++) {
              $shft = 1;
              for ($j=0; $j<$i; $j++) {
                $shft *= $stsubcount2[$j];
              }
              $k2 += $shft*$insubcount2*$ks[$i];
            }
          }
#debug
#print "offset: $k2\n";
          @data2 = split(" ", $range2[$k2]);
          if ($type eq "series" || $TF eq "TRUE") { #leave alone in compose, if FALSE
            $data1[1] = $data2[1]; #change output
            $data1[2] += $data2[2];  #add to run time
            $data1[2] *= $data2[2] if ($Rely); #mult reliability
          }
          if ($type eq "compose") { # only the case where $scount[12] are the same will arise in loops
            if ($TF eq "TRUE") { #not if FALSE
              for ($i=0; $i<$scount1; $i++) {
                $data1[3+$i] = $data2[3+$i];  #replace states, too
              }
              $TF = $data2[3+$scount1];  #use the T/F from the second component
              $data1[3+$scount3] = $TF;
              }
          } else { #series
            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 { #infeasible -- append right number of zeroes
        if ($type ne "compose") { #otherwise doesn't matter, leave alone
          for ($i=0; $i<$scount2; $i++) {
            $data1[3+$scount1+$i] = 0;
          }
        }
      }
      $range3[$k] = join(" ",@data1);
      #nothing more should happen for "compose"
      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" unless ($stateless3);

  #file names used for loop calc
  $theorytest = "once.ccf";
  $theorytest = "once.ccfc" unless ($stateless3);
  $theoryseries = "another.ccf";
  $theoryseries = "another.ccfc" unless ($stateless3);
  $theory = "theory.ccf";
  $theory = "theory.ccfc" unless ($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 an .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 "./CalcS ".$allOptions) {die "`CalcS' script failed"} ;
  $cmd = "mv -f ".$theory." ../".$theorytest;
  `$cmd`;
  chdir ".."; #back to parent directory
#debug
# 
#system "cp $theorytest /tmp/looptest.ccf";

  #check for remaining TRUE subdomains, to unwind again
  open (THEO, $theorytest) || die "Can't open ", $theorytest;
  open (NTHE, ">fixtest") || die "Can't open temp 'fixtest'";
  $head = <THEO>; #header line
  print NTHE $head;  #copy
  unless ($stateless3) {
    @headl = split(" ",$head);
    $moreHlines = $headl[2];  #number of input subd
    for ($s=0; $s<$headl[1]; $s++) {
      $moreHlines += $headl[3+$s];  #number of state subd
    }
    for ($i=1; $i<=$moreHlines; $i++) {
      $tmp = <THEO>;  #skip header lines
      print NTHE $tmp;  #copy
    }
  }
  $anytrue = 0;
  $totalsubs = 0;
  while ($line = <THEO>) {
    chomp($line);
    @isit = split(" ", $line);
    $totalsubs++;
    if ($isit[0] == 0) { #nondata line
      print NTHE "$line\n"; #just copy, LF back
    } else { 
      if ($isit[$itf] eq "TRUE")  {
        $anytrue += 1;
        print NTHE "$line\n";  #copy, put LF back
      }
      else { #came out FALSE
        if ($isit[$itf] ne "FALSE") {
          print "T/F index: $itf\n";
          die "Non-Aristotlian!","$theorytest file; line: $line";
        }
        #adjust runtime/reliability so as not to repeat the test value!
        if ($stateless3) {
          $isit[4] = 0;
          if ($Rely) {
            $isit[5] = 1; #make reliability 1.0
          } else {
            $isit[5] = 0; #make runtime 0
          }
# state case handled by dropping FALSE lines...
#        } else {
#          if ($Rely) {
#            $isit[2] = 1;
#          } else { #run time
#            $isit[2] = 0;
#          }
        }
        $newline = join(" ",@isit);
        print NTHE "$newline\n";
      }
    }
  }
  close(THEO);
  close(NTHE);
  $anytrue1 = $anytrue; #to compare number of subdomains still true after one unwinding
  if ($anytrue) {
    warnmess "  (",$anytrue,"/",$totalsubs," active)";
    system "rm -f $theoryseries; cp $theorytest $theoryseries";
    system "rm -f $theorytest; cp fixtest $theorytest";
  } else {
    warnmess "  (body never executed)";
  }
  system "cp $theorytest $theory";

  while ($anytrue) { #not all the subdomains came out FALSE
    #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
    system "rm -f previouseries; cp $theoryseries previouseries"; #save the old one
    chdir $subdir; #shift to new directory
  #debug -- where are we?
  #print `pwd`;
    #build an .sscf file
    open (SSCF, ">system.sscf") || die "can't create .sscf file for calculation";
    print SSCF "compose\n";
    print SSCF "$theorytest\n";
    print SSCF "$theoryseries\n";
    close SSCF;
#debug
#print `cat system.sscf`;
    if (-1 == system "./CalcS ".$allOptions) {die "`CalcS' script failed"} ;
    $cmd = "mv -f ".$theory." ../".$theoryseries;
    `$cmd`;
#debug
#system "cp $theoryseries /tmp/another"; die "one iteration";
    chdir ".."; #back to parent directory
  
    open (THEO, $theoryseries) || die "can't open $theoryseries";
    #check for remaining TRUE subdomains, to unwind again
    $head = <THEO>; #header line
    unless ($stateless3) {
      @headl = split(" ",$head);
      $itf = 3 + $headl[1];
      $moreHlines = $headl[2];  #number of input subd
      for ($s=0; $s<$headl[1]; $s++) {
        $moreHlines += $headl[3+$s];  #number of state subd
      }
      for ($i=1; $i<=$moreHlines; $i++) {
        $tmp = <THEO>;  #skip header lines
      }
    }

    $anytrue = 0;
    while ($line = <THEO>) {
      @isit = split(" ", $line);
#debug
#print "$line" if ($isit[1] < .1);
      if ($isit[0]>0) { #line with data
        if ($isit[$itf] eq "TRUE")  { 
          $anytrue += 1;
        }
        else { #came out FALSE
          if ($isit[$itf] ne "FALSE") {
            print "T/F index: $itf\n";
            die "Non-Aristotlian!","$theoryseries file; line: $line";
          }
        }
      }
    }
    close(THEO);
    #check for non-termination
    if ($anytrue == $anytrue1) { #same TRUE subdomain count
      #TBD: in case of piecewise-linear and w/state cases this needs checking
      open (THEO, "<$theoryseries") || die "can't open $theoryseries";
      open (PREV, "<previouseries") || die "can't open temp 'previouseries'";
      $head = <THEO>; #header line
      $phead = <PREV>; #header line
      $OK = 0;  #assume that there is a "theory loop"
      $subdlist = "  In subdomain(s):\n"; #message in case of non-termination
      unless ($stateless3) {
        @headl = split(" ",$head);
        $Isubs = $headl[2];  #number of input subd
        @pheadl = split(" ",$phead);
        $pIsubs = $pheadl[2];
        if ($Isubs == $pIsubs) { #same number of input subdomains
          FLS:
          for ($i=0; $i<$Isubs; $i++) {
            $new = <THEO>;  
            @snew = split(" ",$new);
            $old = <PREV>; 
            @sold = split(" ",$old);
            $LBin[$i] = $snew[0];
            $UBin[$i] = $snew[1];
            if ($sold[0] != $snew[0] || $sold[1] != $snew[1]) { #different subd, keep going
              $OK = 1; 
              last FLS;
            }
          }
        } else { #different number of subds
          $OK = 1;
        }
        unless ($OK) { #otherwise the data has not been accumulated
          #TBD accummulate and add to "subdlist" the TRUE ones
          $scount = $headl[1];
          for ($i=0; $i<$scount; $i++) {
            $Ssubs[$i] = $headl[3+$i]; #number of state subdomains
            for ($j=0; $j<$Ssubs[$i]; $j++) {
              $new = <THEO>;
              $old = <PREV>;
              @snew = split(" ",$new);
              $LBst[$i][$j] = $snew[0];
              $UBst[$i][$j] = $snew[1];
            }
          }
          #positioned at the start of data
          $in = 0; #input index
          for ($s=0; $s<$scount; $s++) {
            $st[$s] = 0;  #state indices
          }
          LLL:
          while ($line = <THEO>) {
            @isit = split(" ", $line);
            $lone = <PREV>;
            if (!$lone) { #old file ended sooner, keep going
              $OK = 1;
              last LLL;
            }
            @wasit = split(" ", $lone);
            if ($isit[$itf] ne $wasit[$itf]) { #T/F values differ, keep going
#debug
#print "state T/F difference:\n $line $lone";
              $OK = 1;
              last LLL;
            }
            if ($isit[$itf] eq "TRUE" && $isit[0]) { #feasible & live
              $subdlist .= sprintf("   [%3.2f,%3.2f)", $LBin[$in],$UBin[$in]);
              for ($s=0; $s<$scount; $s++) {
                $subdlist .= sprintf(" X [%3.2f,%3.2f)", $LBst[$s][$st[$s]],$UBst[$s][$st[$s]]);
              }
              $subdlist .= "\n";
            }
            if (++$in>=$Isubs) { #restart input cycle
              $in = 0;
              B2S:
              for ($s=0; $s<$scount; $s++ ) {
                if (++$st[$s] >= $Ssubs[$s]) { #restart state cycle(s)
                  $st[$s] = 0;
                } else { #leave rest alone
                  last B2S;
                }
              }
            }
          } #end loop over data lines
        }
      } else { #stateless
        while ($line = <THEO>) {
          @isit = split(" ", $line);
          unless ($lone = <PREV>) {
            $OK = 1;
          } else {
            @wasit = split(" ", $lone);
            if ($isit[0] != $wasit[0] || $isit[1] != $wasit[1]) { #subd differs, keep going
              $OK = 1;
            }
            if ($isit[$itf] ne $wasit[$itf]) { #$T/F differ
#debug
print "stateless T/F values differ\n $line $lone";
              $OK = 1;
            }
          }
          if ($isit[$itf] eq "TRUE")  {
            $subdlist .= sprintf("   [%3.2f,%3.2f)\n", $isit[0],$isit[1]);
          } 
        }
      }
      close(THEO);
      close(PREV);
      unless ($OK) {
        print $subdlist;
        die "Loop will never terminate (in theory)";
      }
    }
    $thidx++;
    #debug 
    #$theoryname = $theory.$thidx; system "cp $theory /tmp/$theoryname";

    if ($anytrue) {
      warnmess "  Compose: once o again -> again ",$anytrue," subdomains still active";
#debug
#system "cat $theoryseries";
      $anytrue1 = $anytrue; #ready for next iteration
    } else {
      warnmess "  Loop terminated (in theory)";
      system "cp $theoryseries $theory";
    }
  } #end loop over $anytrue
} else { 
  die "Construct type ", $type, " not implemented";
}

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

unless ($type eq "loop") {  #loop file already written above
if ($stateless3) { #result has no state, file is .ccf "theory"
# 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) { #not contiguous, fix
      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";
    }
  }
  #mark off the subdomains that never occur
  for ($k=0; $k<$range3cnt; $k++) { 
    $thcounts[$k] = 0;
  }

  #do the initial state set
  for ($s=0; $s<$scount3; $s++) {
    $stdex[$s] = findindex3($initialState3[$s],$s);
      }
     
  $kk = 0;
  $mul = $insubcount3;
  for ($s=0; $s<$scount3; $s++) {
    $kk += $stdex[$s]*$mul;
    $mul *= $stsubcount3[$s];
  }
  for ($i=0; $i<$insubcount3; $i++) {
    $thcounts[$kk++] += 1;
  }

################################################
sub findindex3 { #locate and return subdomain index for value
  my ($val, $code, $i);
  $val = $_[0];
  $code = $_[1]; # -1 means input
                 # 0..NumStates-1 means that state
  if ($code == -1) { #find input subdomain
    for ($i=0; $i<$insubcount3; $i++) {
      if ($val >= $LBin3[$i] && $val < $UBin3[$i]) {
        return $i;
      }
    }
    die "Input $val not found in subdomains";
  } else { #find state
    for ($i=0; $i<$stsubcount3[$code]; $i++) {
      if ($val >= $LBst3[$code][$i] && $val < $UBst3[$code][$i]) {
        return $i;
      }
    }
    die "State $val not found in state-$code list of subdomains";
  }
}
##############################################
  for ($k=0; $k<$range3cnt; $k++) { 
    @line = split(" ",$range3[$k]);
    if ($line[0]) { #executed, see state where it goes, all inputs (index $kk)
      for ($s=0; $s<$scount3; $s++) {
        $stdex[$s] = findindex3($line[3+$s],$s);
      }
      $kk = 0;
      $mul = $insubcount3;
      for ($s=0; $s<$scount3; $s++) {
        $kk += $stdex[$s]*$mul;
        $mul *= $stsubcount3[$s];
      }
      for ($i=0; $i<$insubcount3; $i++) {
        $thcounts[$kk++] += 1;
      }
    }
  } # end marking live subdomains
  for ($k=0; $k<$range3cnt; $k++) {
    @line = split(" ",$range3[$k]);
#TBD: rethink this...
#   $line[0] = $thcounts[$k];
    $range3[$k] = join(" ",@line);
    print TCCF "$range3[$k]\n";
  }
  close(TCCF);
}
}
