syn_supnorm.h

Go to the documentation of this file.

/** @file syn_supnorm.h Supremal normal sublanguage */
 
/* FAU Discrete Event Systems Library (libfaudes)
 
   Copyright (C) 2009  Sebastian Perk, Thomas Moor
 
   This library is free software; you can redistribute it and/or
   modify it under the terms of the GNU Lesser General Public
   License as published by the Free Software Foundation; either
   version 2.1 of the License, or (at your option) any later version.
 
   This library is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   Lesser General Public License for more details.
 
   You should have received a copy of the GNU Lesser General Public
   License along with this library; if not, write to the Free Software
   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA */
 
 
#ifndef FAUDES_SUPNORM_H
#define FAUDES_SUPNORM_H
 
#include "corefaudes.h"
#include <stack>
 
namespace faudes {
 
/**
 * ConcatenateFullLanguage: concatenate Sigma* to language
 * marked by rGen. Less expensive than using
 * LanguageConcatenate() to concatenate Sigma*, as no
 * additional nondeterminism is caused.
 * Used in SupNorm().
 * Method:
 * Transitions starting from marked states are erased.
 * Remaining accessible marked states are provided with
 * Sigma-selfloops.
 * Determinism:
 * Result can only become nondeterministic when a parameter is
 * nondeterministic.
 *
 * @param rGen
 *   generator marking the language to be concatenated with Sigma*
 * 
 *
 */
extern FAUDES_API void ConcatenateFullLanguage(Generator& rGen);
 
/**
 * NormalityConsistencyCheck: Consistency
 * check for normality input data. Used e.g. in IsNormal(),
 * and SupNorm(). See exceptions.
 *
 * @param rL
 *   generator of language L
 * @param rOAlph
 *   observable alphabet
 * @param rK
 *   generator of language K
 *
 * @exception Exception
 *   - nondeterministic parameter(s) (id: 101)
 *   - rOAlph not subset of rL.Alphabet() (id: 100)
 *   - Alphabets of generators don't match (id: 100)
 *   - K is not subset of L (id 0)
 * 
 *
 */
extern FAUDES_API void NormalityConsistencyCheck(
  const Generator& rL,
  const EventSet& rOAlph,
  const Generator& rK);
 
/**
 * IsNormal: checks normality of a language K generated by
 * rK wrt a language L generated by rL and the subset of
 * observable events rOAlph. This is done by checking if the
 * following equality holds:
 *
 * pinv(p(K)) intersect L \\subseteq K
 * 
 * Thus, we assume K \\subseteq L for a sufficient and necessary test.
 *
 * Todos: 
 * check for efficient algorithm replacing above
 * formula that returns false immediately after having
 * found a non-normal string -> IsNormalFast();
 * implement test routines, verify correctness;
 * compare performance with IsNormalAlt
 *
 * @param rL
 *   generator of language L
 * @param rOAlph
 *   observable alphabet
 * @param rK
 *   generator of language K
 * 
 * @return
 *   true if K is normal w.r.t. L and OAlph
 *
 * @exception Exception
 *   - thrown by NormalityConsistencyCheck()
 * 
 * @ingroup SynthesisPlugIn
 *
 */
extern FAUDES_API bool IsNormal(
  const Generator& rL,
  const EventSet& rOAlph,
  const Generator& rK);
 
/** 
 * IsNormal wrapper.  
 * Wrapper for convenient access via the run-time interface.
 */
extern FAUDES_API bool IsNormal(const System& rPlantGen, const Generator& rSupCandGen);
 
 
/**
 * SupNorm: compute supremal normal sublanguage.
 *
 * SupNorm calculates the supremal sublanguage
 * of the closed language K (generated by rK)
 * that is normal w.r.t. the closed language L
 * (generated by rL) and the set
 * of observable events.
 *
 * Method: The supremal normal sublanguage is computed
 * according to the Lin-Brandt-Formula:
 * supnorm(K)wrt(L)=K-Pinv[P(L-K)]
 *
 * SupNorm returns false on empty result.
 *
 * Parameters have to be deterministic, result is deterministic.
 *
 *
 * @param rL
 *   generates the closed language L=L(rL)
 * @param rOAlph
 *   observable alphabet
 * @param rK
 *   generates the closed language K=L(rK)
 * @param rResult
 *   marks the supremal normal
 *   sublanguage (not necessaryly prefix closed)
 * 
 * @return
 *   true for nonempty result
 *
 * @exception Exception
 *   - Alphabets of generators don't match (id 500)
 *   - rOAlph not subset of rL.Alphabet() (id 506)
 *   - K is not subset of L. (id 0)
 *
 * @ingroup SynthesisPlugIn
 * 
 *
 */
extern FAUDES_API bool SupNorm(
  const Generator& rL,
  const EventSet& rOAlph,
  const Generator& rK, 
  Generator& rResult);
 
 
/**
 * SupNormClosed - compute supremal normal and closed
 * sublanguage. 
 *
 * SupNormClosed calculates the supremal sublanguage
 * of the closed language K (generated by rK)
 * that is closed  and normal w.r.t. the closed language
 * L (generated by rL) and the set
 * of observable events.
 *
 * Method: The supremal normal sublanguage is computed
 * according to the Lin-Brandt-Formula:
 * supnormclosed(K)wrt(L)=K-Pinv[P(L-K)]Sigma*
 *
 * Parameters have to be deterministic, result is deterministic.
 *
 *
 * @param rL
 *   generates the closed language L=L(rL)
 * @param rOAlph
 *   observable alphabet
 * @param rK
 *   generates the closed language K=L(rK)
 * @param rResult
 *   marks and generates the supremal normal and closed
 *   sublanguage
 * 
 * @return
 *   true for nonempty result
 *
 * @exception Exception
 *   - Alphabets of generators don't match (id 500)
 *   - rOAlph not subset of rL.Alphabet() (id 506)
 *   - K is not subset of L. (id 0)
 *
 * @ingroup SynthesisPlugIn
 * 
 *
 */
extern FAUDES_API bool SupNormClosed(
  const Generator& rL,
  const EventSet& rOAlph,
  const Generator& rK, 
  Generator& rResult);
 
 
/**
 * SupConNormClosed: compute supremal controllable, normal and closed
 * sublanguage.
 *
 * SupConNormClosed computes the supremal sublanguage
 * of language K (generated by rK) that is
 * - controllable w.r.t. the language L (generated by rL);
 * - normal w.r.t. the language L; and 
 * - prefix closed.
 *
 * The implementation is based on results by Brandt et al 
 * "Formulas for calculation supremal and normal sublanguages", 
 * Thm 4, System and Control Letters, 1990.
 *
 * Parameters have to be deterministic, result is deterministic.
 *
 *
 * @param rL
 *   generates the closed language L=L(rL)
 * @param rCAlph
 *   controllable alphabet
 * @param rOAlph
 *   observable alphabet
 * @param rK
 *   generates the closed language K=L(rK)
 * @param rResult
 *   marks and generates the supremal contr, normal and closed
 *   sublanguage 
 * 
 *
 * @exception Exception
 *   - Alphabets of generators don't match (id 500)
 *   - rCAlph not subset of rL.Alphabet() (id 506)
 *   - rOAlph not subset of rL.Alphabet() (id 506)
 *   - K is not subset of L. (id 0)
 *
 * @ingroup SynthesisPlugIn
 * 
 *
 */
extern FAUDES_API void SupConNormClosed(
  const Generator& rL,
  const EventSet& rCAlph,
  const EventSet& rOAlph,
  const Generator& rK, 
  Generator& rResult);
 
 
/**
 * Supremal Normal Controllable Sublangauge (internal function)
 *
 * Indentifies and deletes conflicting transitions to obtain a controllable and
 * prefix-normal sublanguage. This function is a bit experimental it depends on various 
 * unverified preconditions and conjectures -- use only after careful code-review. 
 * The completely independent implementation SupNormConClosed should be fine
 * 
 * Conditions
 * - controllabel events as specified explicitly must be a subset of the observable events
 * - L(H) <= L(G) 
 * - stateset of H must be sufficiently rich to discriminate states in G (e.g. initialise by H:=H' x G) 
 * - H_obs must be "a" observer automaton for H w.r.t. observable events (e.g. initialize with p_inv p H)
 *
 * @param rPlantGen
 *   Plant generator G
 * @param rCAlph
 *   Controllable events
 * @param rOAlph
 *   Observable events
 * @param rObserverGen
 *   Observer H_obs
 * @param rSupCandGen
 *   Closed-loop candidate H
 *
 *
 */
extern FAUDES_API void SupConNormClosedUnchecked(
   const Generator& rPlantGen, 
   const EventSet&  rCAlph,
   const EventSet&  rOAlph,
   Generator& rObserverGen,     
   Generator& rSupCandGen);
 
 
/**
 * SupConNormNB: compute supremal controllable and normal sublanguage
 *
 * SupConNormNB computes the supremal sublanguage
 * of language K (marked by rK) that 
 * - is controllable w.r.t. the language L (marked by rL);
 * - has a prefix closure that is normal w.r.t. the closure of L
 *
 * The implementation is based on results by Yoo, Lafortune and Lin 
 * "A uniform approach for computing supremal sublanguages arising 
 * in supervisory control theory", 2002.
 *
 * Parameters have to be deterministic, result is deterministic.
 *
 *
 * @param rL
 *   generates the closed language L=L(rL)
 * @param rCAlph
 *   controllable alphabet
 * @param rOAlph
 *   observable alphabet
 * @param rK
 *   generates the closed language K=L(rK)
 * @param rResult
 *   marks the supremal normal and controllable
 *   sublanguage
 * 
 *
 * @exception Exception
 *   - Alphabets of generators don't match (id 500)
 *   - rCAlph not subset of rL.Alphabet() (id 506)
 *   - rOAlph not subset of rL.Alphabet() (id 506)
 *   - K is not subset of L. (id 0)
 *
 * @ingroup SynthesisPlugIn
 * 
 *
 */
extern FAUDES_API void SupConNormNB(
  const Generator& rL,
  const EventSet& rCAlph,
  const EventSet& rOAlph,
  const Generator& rK, 
  Generator& rResult);
 
 
/**
 * SupPrefixClosed: supremal closed sublanguage of K by cancelling
 * all tranistions leading to a non-marked state.
 * Returns false on empty result.
 * todo: implement test routines, verify correctness
 *
 * @param rK
 *   marks the (not necessarily closed) language K=Lm(rK)
 * @param rResult
 *   generates and marks the supremal closed sublanguage,
 *   where L(rResult)=Lm(rResult)
 * 
 * @return
 *   true for nonempty result
 *
 * @exception Exception
 *   - todo: check determinism of rK
 * 
 *
 */
extern FAUDES_API bool SupPrefixClosed(
  const Generator& rK,
  Generator& rResult);
 
 
/** rti wrapper */
extern FAUDES_API void SupNorm(
  const System& rPlantGen, 
  const Generator& rSpecGen, 
  Generator& rResGen);
 
 
/** rti wrapper */
extern FAUDES_API void SupNormClosed(
  const System& rPlantGen, 
  const Generator& rSpecGen, 
  Generator& rResGen);
 
/** rti wrapper */
extern FAUDES_API void SupConNormClosed(
  const System& rPlantGen, 
  const Generator& rSpecGen, 
  Generator& rResGen);
 
/** rti wrapper */
extern FAUDES_API void SupConNormNB(
  const System& rPlantGen, 
  const Generator& rSpecGen, 
  Generator& rResGen);
 
 
} // end namespace
#endif